feat(topology/separation): add t1_space_tfae (#11534)

Also add some lemmas about `filter.disjoint`.

src/order/filter/bases.lean

@@ -454,6 +454,11 @@ lemma has_basis.inf_principal_ne_bot_iff (hl : l.has_basis p s) {t : set α} :
   ne_bot (l ⊓ 𝓟 t) ↔ ∀ ⦃i⦄ (hi : p i), (s i ∩ t).nonempty :=
 (hl.inf_principal t).ne_bot_iff
 
+lemma has_basis.disjoint_basis_iff (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
+  disjoint l l' ↔ ∃ i (hi : p i) i' (hi' : p' i'), disjoint (s i) (s' i') :=
+not_iff_not.mp $ by simp only [disjoint_iff, ← ne.def, ← ne_bot_iff, hl.inf_basis_ne_bot_iff hl',
+  not_exists, bot_eq_empty, ne_empty_iff_nonempty, inf_eq_inter]
+
 lemma inf_ne_bot_iff :
   ne_bot (l ⊓ l') ↔ ∀ ⦃s : set α⦄ (hs : s ∈ l) ⦃s'⦄ (hs' : s' ∈ l'), (s ∩ s').nonempty :=
 l.basis_sets.inf_ne_bot_iff
@@ -462,15 +467,6 @@ lemma inf_principal_ne_bot_iff {s : set α} :
   ne_bot (l ⊓ 𝓟 s) ↔ ∀ U ∈ l, (U ∩ s).nonempty :=
 l.basis_sets.inf_principal_ne_bot_iff
 
-lemma inf_eq_bot_iff {f g : filter α} :
-  f ⊓ g = ⊥ ↔ ∃ (U ∈ f) (V ∈ g), U ∩ V = ∅ :=
-not_iff_not.1 $ ne_bot_iff.symm.trans $ inf_ne_bot_iff.trans $
-by simp [← ne_empty_iff_nonempty]
-
-protected lemma disjoint_iff {f g : filter α} :
-  disjoint f g ↔ ∃ (U ∈ f) (V ∈ g), U ∩ V = ∅ :=
-disjoint_iff.trans inf_eq_bot_iff
-
 lemma mem_iff_inf_principal_compl {f : filter α} {s : set α} :
   s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥ :=
 begin
@@ -483,13 +479,23 @@ lemma not_mem_iff_inf_principal_compl {f : filter α} {s : set α} :
   s ∉ f ↔ ne_bot (f ⊓ 𝓟 sᶜ) :=
 (not_congr mem_iff_inf_principal_compl).trans ne_bot_iff.symm
 
-lemma mem_iff_disjoint_principal_compl {f : filter α} {s : set α} :
-  s ∈ f ↔ disjoint f (𝓟 sᶜ) :=
-mem_iff_inf_principal_compl.trans disjoint_iff.symm
+@[simp] lemma disjoint_principal_right {f : filter α} {s : set α} :
+  disjoint f (𝓟 s) ↔ sᶜ ∈ f :=
+by rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]
+
+@[simp] lemma disjoint_principal_left {f : filter α} {s : set α} :
+  disjoint (𝓟 s) f ↔ sᶜ ∈ f :=
+by rw [disjoint.comm, disjoint_principal_right]
+
+@[simp] lemma disjoint_principal_principal {s t : set α} :
+  disjoint (𝓟 s) (𝓟 t) ↔ disjoint s t :=
+by simp [disjoint_iff_subset_compl_left]
+
+alias disjoint_principal_principal ↔ _ disjoint.filter_principal
 
-lemma le_iff_forall_disjoint_principal_compl {f g : filter α} :
-  f ≤ g ↔ ∀ V ∈ g, disjoint f (𝓟 Vᶜ) :=
-forall₂_congr $ λ _ _, mem_iff_disjoint_principal_compl
+@[simp] lemma disjoint_pure_pure {x y : α} :
+  disjoint (pure x : filter α) (pure y) ↔ x ≠ y :=
+by simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]
 
 lemma le_iff_forall_inf_principal_compl {f g : filter α} :
   f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥ :=

src/order/filter/basic.lean

@@ -589,13 +589,18 @@ lemma compl_not_mem {f : filter α} {s : set α} [ne_bot f] (h : s ∈ f) : sᶜ
 lemma filter_eq_bot_of_is_empty [is_empty α] (f : filter α) : f = ⊥ :=
 empty_mem_iff_bot.mp $ univ_mem' is_empty_elim
 
+protected lemma disjoint_iff {f g : filter α} :
+  disjoint f g ↔ ∃ (s ∈ f) (t ∈ g), disjoint s t :=
+by simp only [disjoint_iff, ← empty_mem_iff_bot, mem_inf_iff,
+  inf_eq_inter, bot_eq_empty, @eq_comm _ ∅]
+
 lemma disjoint_of_disjoint_of_mem {f g : filter α} {s t : set α} (h : disjoint s t)
   (hs : s ∈ f) (ht : t ∈ g) : disjoint f g :=
-begin
-  refine le_of_eq (empty_mem_iff_bot.1 _),
-  rw [← set.disjoint_iff_inter_eq_empty.1 h],
-  exact inter_mem_inf hs ht
-end
+filter.disjoint_iff.mpr ⟨s, hs, t, ht, h⟩
+
+lemma inf_eq_bot_iff {f g : filter α} :
+  f ⊓ g = ⊥ ↔ ∃ (U ∈ f) (V ∈ g), U ∩ V = ∅ :=
+by simpa only [disjoint_iff] using filter.disjoint_iff
 
 /-- There is exactly one filter on an empty type. --/
 -- TODO[gh-6025]: make this globally an instance once safe to do so
@@ -1853,7 +1858,7 @@ hf.comap_of_range_mem $ mem_of_superset hs (image_subset_range _ _)
 
 @[simp] lemma map_eq_bot_iff : map m f = ⊥ ↔ f = ⊥ :=
 ⟨by { rw [←empty_mem_iff_bot, ←empty_mem_iff_bot], exact id },
-  λ h, by simp only [h, eq_self_iff_true, map_bot]⟩
+  λ h, by simp only [h, map_bot]⟩
 
 lemma map_ne_bot_iff (f : α → β) {F : filter α} : ne_bot (map f F) ↔ ne_bot F :=
 by simp only [ne_bot_iff, ne, map_eq_bot_iff]

src/topology/algebra/ordered/basic.lean

@@ -1148,10 +1148,9 @@ end pi
 lemma disjoint_nhds_at_top [no_max_order α] (x : α) :
   disjoint (𝓝 x) at_top :=
 begin
-  rw filter.disjoint_iff,
-  cases exists_gt x with a ha,
-  use [Iio a, Iio_mem_nhds ha, Ici a, mem_at_top a],
-  rw [inter_comm, Ici_inter_Iio, Ico_self]
+  rcases exists_gt x with ⟨y, hy : x < y⟩,
+  refine disjoint_of_disjoint_of_mem _ (Iio_mem_nhds hy) (mem_at_top y),
+  exact disjoint_left.mpr (λ z, not_le.2)
 end
 
 @[simp] lemma inf_nhds_at_top [no_max_order α] (x : α) :
@@ -1183,7 +1182,7 @@ hf.not_tendsto (disjoint_nhds_at_bot x).symm
 
 lemma not_tendsto_at_bot_of_tendsto_nhds [no_min_order α]
   {F : filter β} [ne_bot F] {f : β → α} {x : α} (hf : tendsto f F (𝓝 x)) :
-  ¬  tendsto f F at_bot :=
+  ¬ tendsto f F at_bot :=
 hf.not_tendsto (disjoint_nhds_at_bot x)
 
 /-!

src/topology/separation.lean

@@ -19,7 +19,7 @@ This file defines the predicate `separated`, and common separation axioms
   there is an open set that contains one, but not the other.
 * `t1_space`: A T₁/Fréchet space is a space where every singleton set is closed.
   This is equivalent to, for every pair `x ≠ y`, there existing an open set containing `x`
-  but not `y` (`t1_iff_exists_open` shows that these conditions are equivalent.)
+  but not `y` (`t1_space_iff_exists_open` shows that these conditions are equivalent.)
 * `t2_space`: A T₂/Hausdorff space is a space where, for every two points `x ≠ y`,
   there is two disjoint open sets, one containing `x`, and the other `y`.
 * `t2_5_space`: A T₂.₅/Urysohn space is a space where, for every two points `x ≠ y`,
@@ -278,13 +278,6 @@ class t1_space (α : Type u) [topological_space α] : Prop :=
 lemma is_closed_singleton [t1_space α] {x : α} : is_closed ({x} : set α) :=
 t1_space.t1 x
 
-lemma finite.is_closed [t1_space α] {s : set α} (hs : set.finite s) :
-  is_closed s :=
-begin
-  rw ← bUnion_of_singleton s,
-  exact is_closed_bUnion hs (λ i hi, is_closed_singleton)
-end
-
 lemma is_open_compl_singleton [t1_space α] {x : α} : is_open ({x}ᶜ : set α) :=
 is_closed_singleton.is_open_compl
 
@@ -302,36 +295,78 @@ begin
   exact mem_nhds_within_of_mem_nhds (is_open_ne.mem_nhds h)
 end
 
-@[priority 100] -- see Note [lower instance priority]
-instance t1_space_cofinite {α : Type*} : @t1_space α (cofinite_topology α) :=
+protected lemma set.finite.is_closed [t1_space α] {s : set α} (hs : set.finite s) :
+  is_closed s :=
 begin
-  letI := cofinite_topology α,
-  constructor,
-  intros x,
-  rw ← is_open_compl_iff,
-  intro h,
-  simp,
+  rw ← bUnion_of_singleton s,
+  exact is_closed_bUnion hs (λ i hi, is_closed_singleton)
 end
 
-lemma t1_space_antimono {α : Type*} : antitone (@t1_space α) :=
+protected lemma finset.is_closed [t1_space α] (s : finset α) : is_closed (s : set α) :=
+s.finite_to_set.is_closed
+
+lemma t1_space_tfae (α : Type u) [t : topological_space α] :
+  tfae [t1_space α,
+    ∀ x, is_closed ({x} : set α),
+    ∀ x, is_open ({x}ᶜ : set α),
+    t ≤ cofinite_topology α,
+    ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
+    ∀ ⦃x y : α⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
+    ∀ ⦃x y : α⦄, x ≠ y → ∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U,
+    ∀ ⦃x y : α⦄, x ≠ y → disjoint (𝓝 x) (pure y),
+    ∀ ⦃x y : α⦄, x ≠ y → disjoint (pure x) (𝓝 y)] :=
 begin
-  rintros t t' h ⟨ht⟩,
-  constructor,
-  intros x,
-  specialize ht x,
-  rw ← is_open_compl_iff at *,
-  exact h _ ht
+  tfae_have : 1 ↔ 2, from ⟨λ h, h.1, λ h, ⟨h⟩⟩,
+  tfae_have : 2 ↔ 3, by simp only [is_open_compl_iff],
+  tfae_have : 5 ↔ 3,
+  { refine forall_swap.trans _,
+    simp only [is_open_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, exists_prop, and.assoc,
+      and.left_comm],
+  tfae_have : 5 ↔ 8,
+    by simp only [← principal_singleton, disjoint_principal_right],
+  tfae_have : 8 ↔ 9, from forall_swap.trans (by simp only [disjoint.comm, ne_comm]),
+  tfae_have : 1 → 4,
+  { introsI H s hs,
+    simp only [cofinite_topology, ← ne_empty_iff_nonempty, ne.def, ← or_iff_not_imp_left] at hs,
+    rcases hs with rfl | hs,
+    exacts [is_open_empty, compl_compl s ▸ hs.is_closed.is_open_compl] },
+  tfae_have : 4 → 3,
+  { refine λ h x, h _ (λ _, _), simp },
+  tfae_finish
 end
 
 lemma t1_space_iff_le_cofinite {α : Type*} [t : topological_space α] :
   t1_space α ↔ t ≤ cofinite_topology α :=
+(t1_space_tfae α).out 0 3
+
+lemma t1_space_iff_exists_open : t1_space α ↔
+  ∀ (x y), x ≠ y → (∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U) :=
+(t1_space_tfae α).out 0 6
+
+lemma t1_space_iff_disjoint_pure_nhds : t1_space α ↔ ∀ ⦃x y : α⦄, x ≠ y → disjoint (pure x) (𝓝 y) :=
+(t1_space_tfae α).out 0 8
+
+lemma t1_space_iff_disjoint_nhds_pure : t1_space α ↔ ∀ ⦃x y : α⦄, x ≠ y → disjoint (𝓝 x) (pure y) :=
+(t1_space_tfae α).out 0 7
+
+lemma disjoint_pure_nhds [t1_space α] {x y : α} (h : x ≠ y) : disjoint (pure x) (𝓝 y) :=
+t1_space_iff_disjoint_pure_nhds.mp ‹_› h
+
+lemma disjoint_nhds_pure [t1_space α] {x y : α} (h : x ≠ y) : disjoint (𝓝 x) (pure y) :=
+t1_space_iff_disjoint_nhds_pure.mp ‹_› h
+
+@[priority 100] -- see Note [lower instance priority]
+instance t1_space_cofinite {α : Type*} : @t1_space α (cofinite_topology α) :=
+(@t1_space_iff_le_cofinite α (cofinite_topology α)).mpr le_rfl
+
+lemma t1_space_antitone {α : Type*} : antitone (@t1_space α) :=
 begin
-  split,
-  { introsI h U U_op,
-    rcases U.eq_empty_or_nonempty with rfl | hU,
-    { exact is_open_empty },
-    { exact (@is_closed_compl_iff α t U).mp (finite.is_closed $ U_op hU) } },
-  { exact λ h, t1_space_antimono h t1_space_cofinite }
+  simp only [antitone, t1_space_iff_le_cofinite],
+  exact λ t₁ t₂ h, h.trans
 end
 
 lemma continuous_within_at_update_of_ne [t1_space α] [decidable_eq α] [topological_space β]
@@ -372,30 +407,6 @@ instance subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p
 instance t1_space.t0_space [t1_space α] : t0_space α :=
 ⟨λ x y h, ⟨{z | z ≠ y}, is_open_ne, or.inl ⟨h, not_not_intro rfl⟩⟩⟩
 
-lemma t1_iff_exists_open : t1_space α ↔
-  ∀ (x y), x ≠ y → (∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U) :=
-begin
-  split,
-  { introsI t1 x y hxy,
-    exact ⟨{y}ᶜ, is_open_compl_iff.mpr (t1_space.t1 y),
-            mem_compl_singleton_iff.mpr hxy,
-            not_not.mpr rfl⟩},
-  { intro h,
-    constructor,
-    intro x,
-    rw ← is_open_compl_iff,
-    have p : ⋃₀ {U : set α | (x ∉ U) ∧ (is_open U)} = {x}ᶜ,
-    { apply subset.antisymm; intros t ht,
-      { rcases ht with ⟨A, ⟨hxA, hA⟩, htA⟩,
-        rw [mem_compl_eq, mem_singleton_iff],
-        rintro rfl,
-        contradiction },
-      { obtain ⟨U, hU, hh⟩ := h t x (mem_compl_singleton_iff.mp ht),
-        exact ⟨U, ⟨hh.2, hU⟩, hh.1⟩}},
-    rw ← p,
-    exact is_open_sUnion (λ B hB, hB.2) }
-end
-
 lemma compl_singleton_mem_nhds [t1_space α] {x y : α} (h : y ≠ x) : {x}ᶜ ∈ 𝓝 y :=
 is_open_compl_singleton.mem_nhds $ by rwa [mem_compl_eq, mem_singleton_iff]
 
@@ -485,20 +496,12 @@ infinite. -/
 lemma infinite_of_mem_nhds {α} [topological_space α] [t1_space α] (x : α) [hx : ne_bot (𝓝[≠] x)]
   {s : set α} (hs : s ∈ 𝓝 x) : set.infinite s :=
 begin
-  unfreezingI { contrapose! hx },
-  rw set.not_infinite at hx,
-  have A : is_closed (s \ {x}) := finite.is_closed (hx.subset (diff_subset _ _)),
-  have B : (s \ {x})ᶜ ∈ 𝓝 x,
-  { apply is_open.mem_nhds,
-    { apply is_open_compl_iff.2 A },
-    { simp only [not_true, not_false_iff, mem_diff, and_false, mem_compl_eq, mem_singleton] } },
-  have C : {x} ∈ 𝓝 x,
-  { apply filter.mem_of_superset (filter.inter_mem hs B),
-    assume y hy,
-    simp only [mem_singleton_iff, mem_inter_eq, not_and, not_not, mem_diff, mem_compl_eq] at hy,
-    simp only [hy.right hy.left, mem_singleton] },
-  have D : {x}ᶜ ∈ 𝓝[≠] x := self_mem_nhds_within,
-  simpa [← empty_mem_iff_bot] using filter.inter_mem (mem_nhds_within_of_mem_nhds C) D
+  intro hsf,
+  have A : {x} ⊆ s, by simp only [singleton_subset_iff, mem_of_mem_nhds hs],
+  have B : is_closed (s \ {x}) := (hsf.subset (diff_subset _ _)).is_closed,
+  have C : (s \ {x})ᶜ ∈ 𝓝 x, from B.is_open_compl.mem_nhds (λ h, h.2 rfl),
+  have D : {x} ∈ 𝓝 x, by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C,
+  rwa [← mem_interior_iff_mem_nhds, interior_singleton] at D
 end
 
 lemma discrete_of_t1_of_finite {X : Type*} [topological_space X] [t1_space X] [fintype X] :
@@ -507,7 +510,7 @@ begin
   apply singletons_open_iff_discrete.mp,
   intros x,
   rw [← is_closed_compl_iff],
-  exact finite.is_closed (finite.of_fintype _)
+  exact (finite.of_fintype _).is_closed
 end
 
 lemma singleton_mem_nhds_within_of_mem_discrete {s : set α} [discrete_topology s]
@@ -1104,7 +1107,7 @@ class regular_space (α : Type u) [topological_space α] extends t0_space α : P
 @[priority 100] -- see Note [lower instance priority]
 instance regular_space.t1_space [regular_space α] : t1_space α :=
 begin
-  rw t1_iff_exists_open,
+  rw t1_space_iff_exists_open,
   intros x y hxy,
   obtain ⟨U, hU, h⟩ := t0_space.t0 x y hxy,
   cases h,