English
The T1 space property is equivalent to a long list of equivalent conditions, including that singletons are closed, complements of singletons are open, open sets separate points, disjointness relations of nhds and pure, and T0/R0 properties.
Русский
Свойство T1-пространства эквивалентно длинному списку эквивалентных условий, включая замкнутость одиночек, открытость комплементов одиночек, возможность разделять точки открытыми множествами и др.
LaTeX
$$$ T1Space(X) \\iff \\bigwedge_{i=1}^{12} P_i(X) $, где P_i перечисляет перечисленные условия из TFAE.$$
Lean4
theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] :
List.TFAE
[T1Space X, ∀ x, IsClosed ({ x } : Set X), ∀ x, IsOpen ({ x }ᶜ : Set X), Continuous (@CofiniteTopology.of X),
∀ ⦃x y : X⦄, x ≠ y → { y }ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
∀ ⦃x y : X⦄, x ≠ y → ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X] :=
by
tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
tfae_have 2 ↔ 3 := by simp only [isOpen_compl_iff]
tfae_have 5 ↔ 3 := by
refine forall_swap.trans ?_
simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]
tfae_have 5 ↔ 6 := by simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]
tfae_have 5 ↔ 7 := by simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, and_assoc, and_left_comm]
tfae_have 5 ↔ 8 := by simp only [← principal_singleton, disjoint_principal_right]
tfae_have 8 ↔ 9 := forall_swap.trans (by simp only [disjoint_comm, ne_comm])
tfae_have 1 → 4 := by
simp only [continuous_def, CofiniteTopology.isOpen_iff']
rintro H s (rfl | hs)
exacts [isOpen_empty, compl_compl s ▸ (@Set.Finite.isClosed _ _ H _ hs).isOpen_compl]
tfae_have 4 → 2 := fun h x => (CofiniteTopology.isClosed_iff.2 <| Or.inr (finite_singleton _)).preimage h
tfae_have 2 ↔ 10 := by
simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def, mem_singleton_iff, eq_comm]
tfae_have 10 ↔ 11 :=
⟨fun h => ⟨⟨fun _ _ h₂ => h h₂.specializes⟩, ⟨fun _ _ h₂ => specializes_of_eq (h h₂).symm⟩⟩, fun ⟨_, _⟩ _ _ h =>
(h.antisymm h.symm).eq⟩
tfae_finish
