English
Let X be a normal topological space. If s and t are disjoint, t is closed, and t is a Gδ set, then there exists a separating cover of s and t.
Русский
Пусть X — нормальное топологическое пространство. Если s и t не пересекаются, t замкнуто и t является множества Gδ, то существует разделяющее покрытие множеств s и t.
LaTeX
$$$ \operatorname{NormalSpace}(X) \land s \cap t = \varnothing \land \operatorname{IsClosed}(t) \land \operatorname{IsG\delta}(t) \Rightarrow \operatorname{HasSeparatingCover}(s,t) $$$
Lean4
/-- Lemma that allows the easy conclusion that perfectly normal spaces are completely normal. -/
theorem hasSeparatingCover_closed_gdelta_right {s t : Set X} [NormalSpace X] (st_dis : Disjoint s t) (t_cl : IsClosed t)
(t_gd : IsGδ t) : HasSeparatingCover s t :=
by
obtain ⟨T, T_open, T_count, T_int⟩ := t_gd
rcases T.eq_empty_or_nonempty with rfl | T_nonempty
· rw [T_int, sInter_empty] at st_dis
rw [(s.disjoint_univ).mp st_dis]
exact t.hasSeparatingCover_empty_left
obtain ⟨g, g_surj⟩ := T_count.exists_surjective T_nonempty
choose g' g'_open clt_sub_g' clg'_sub_g using fun n ↦
by
apply normal_exists_closure_subset t_cl (T_open (g n).1 (g n).2)
rw [T_int]
exact sInter_subset_of_mem (g n).2
have clg'_int : t = ⋂ i, closure (g' i) :=
by
apply (subset_iInter fun n ↦ (clt_sub_g' n).trans subset_closure).antisymm
rw [T_int]
refine subset_sInter fun t tinT ↦ ?_
obtain ⟨n, gn⟩ := g_surj ⟨t, tinT⟩
refine iInter_subset_of_subset n <| (clg'_sub_g n).trans ?_
rw [gn]
use fun n ↦ (closure (g' n))ᶜ
constructor
· rw [← compl_iInter, subset_compl_comm, ← clg'_int]
exact st_dis.subset_compl_left
· refine fun n ↦ ⟨isOpen_compl_iff.mpr isClosed_closure, ?_⟩
simp only [closure_compl, disjoint_compl_left_iff_subset]
rw [← closure_eq_iff_isClosed.mpr t_cl] at clt_sub_g'
exact subset_closure.trans <| (clt_sub_g' n).trans <| (g'_open n).subset_interior_closure
