[STATEMENT]
lemma (in topological_space) at_within_union:
  "at x within (S \<union> T) = sup (at x within S) (at x within T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at x within S \<union> T = sup (at x within S) (at x within T)
[PROOF STEP]
unfolding filter_eq_iff eventually_sup eventually_at_filter
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P. (\<forall>\<^sub>F xa in nhds x. xa \<noteq> x \<longrightarrow> xa \<in> S \<union> T \<longrightarrow> P xa) = ((\<forall>\<^sub>F xa in nhds x. xa \<noteq> x \<longrightarrow> xa \<in> S \<longrightarrow> P xa) \<and> (\<forall>\<^sub>F xa in nhds x. xa \<noteq> x \<longrightarrow> xa \<in> T \<longrightarrow> P xa))
[PROOF STEP]
by (auto elim!: eventually_rev_mp)