English
Let s and t be subsets of a topological space X. The statement says that having separating covers in both directions is equivalent to s and t being separated in the neighbourhood sense, i.e., there exist families of open sets that separate s from t in both directions.
Русский
Пусть s и t — подмножества топологического пространства X. Утверждение говорит, что существование разделяющих покрытий в обе стороны эквивалентно тому, что s и t разделены в окрестностной системе: существуют семейства открытых множеств, которые разделяют s и t в обе стороны.
LaTeX
$$$ (\mathrm{HasSeparatingCover}(s,t) \land \mathrm{HasSeparatingCover}(t,s)) \iff \mathrm{SeparatedNhds}(s,t) $$$
Lean4
/-- Used to prove that a regular topological space with Lindelöf topology is a normal space,
and a perfectly normal space is a completely normal space. -/
theorem hasSeparatingCovers_iff_separatedNhds {s t : Set X} :
HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t :=
by
constructor
· rintro ⟨⟨u, u_cov, u_props⟩, ⟨v, v_cov, v_props⟩⟩
have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) → IsOpen (⋃ n, u₀ n \ closure (a n)) :=
fun _ _ u₀i_open ↦ isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure
have cover_lemma :
∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
(h₀ ⊆ ⋃ n, u₀ n) → (∀ n, Disjoint (closure (v₀ n)) h₀) → (h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m ≤ n, v₀ m)) :=
fun h₀ u₀ v₀ h₀_cov dis x xinh ↦ by
rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩
simp only [mem_iUnion]
refine ⟨n, xinun, ?_⟩
simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_iUnion, exists_false, not_false_eq_true]
refine
⟨⋃ n : ℕ, u n \ (closure (⋃ m ≤ n, v m)), ⋃ n : ℕ, v n \ (closure (⋃ m ≤ n, u m)),
open_lemma u (fun n ↦ ⋃ m ≤ n, v m) (fun n ↦ (u_props n).1),
open_lemma v (fun n ↦ ⋃ m ≤ n, u m) (fun n ↦ (v_props n).1), cover_lemma s u v u_cov (fun n ↦ (v_props n).2),
cover_lemma t v u v_cov (fun n ↦ (u_props n).2), ?_⟩
rw [Set.disjoint_left]
rintro x ⟨un, ⟨n, rfl⟩, xinun⟩
suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa
intro m xinvm
have n_le_m : n ≤ m := by
by_contra m_gt_n
exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))
exact subset_closure (mem_biUnion n_le_m xinun.1)
· rintro ⟨U, V, U_open, V_open, h_sub_U, k_sub_V, UV_dis⟩
exact
⟨⟨fun _ ↦ U, h_sub_U.trans (iUnion_const U).symm.subset, fun _ ↦
⟨U_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) k_sub_V (UV_dis.closure_left V_open)⟩⟩,
⟨fun _ ↦ V, k_sub_V.trans (iUnion_const V).symm.subset, fun _ ↦
⟨V_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) h_sub_U (UV_dis.closure_right U_open).symm⟩⟩⟩
