feat(topology/separation): define regular_space (#16360)

src/analysis/locally_convex/balanced_core_hull.lean

@@ -245,7 +245,7 @@ filter.has_basis_self.mpr
   (λ s hs, ⟨balanced_core 𝕜 s, balanced_core_mem_nhds_zero hs,
             balanced_core_balanced s, balanced_core_subset s⟩)
 
-lemma nhds_basis_closed_balanced [t3_space E] : (𝓝 (0 : E)).has_basis
+lemma nhds_basis_closed_balanced [regular_space E] : (𝓝 (0 : E)).has_basis
   (λ (s : set E), s ∈ 𝓝 (0 : E) ∧ is_closed s ∧ balanced 𝕜 s) id :=
 begin
   refine (closed_nhds_basis 0).to_has_basis (λ s hs, _) (λ s hs, ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩),

src/order/filter/bases.lean

@@ -606,6 +606,15 @@ by simp only [← principal_singleton, disjoint_principal_principal, disjoint_si
   (diagonal α)ᶜ ∈ l₁ ×ᶠ l₂ ↔ disjoint l₁ l₂ :=
 by simp only [mem_prod_iff, filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]
 
+lemma has_basis.disjoint_iff_left (h : l.has_basis p s) :
+  disjoint l l' ↔ ∃ i (hi : p i), (s i)ᶜ ∈ l' :=
+by simp only [h.disjoint_iff l'.basis_sets, exists_prop, id, ← disjoint_principal_left,
+  (has_basis_principal _).disjoint_iff l'.basis_sets, unique.exists_iff]
+
+lemma has_basis.disjoint_iff_right (h : l.has_basis p s) :
+  disjoint l' l ↔ ∃ i (hi : p i), (s i)ᶜ ∈ l' :=
+disjoint.comm.trans h.disjoint_iff_left
+
 lemma le_iff_forall_inf_principal_compl {f g : filter α} :
   f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥ :=
 forall₂_congr $ λ _ _, mem_iff_inf_principal_compl

src/topology/algebra/group.lean

@@ -996,28 +996,27 @@ variables (G) [topological_space G] [group G] [topological_group G]
 lemma topological_group.t1_space (h : @is_closed G _ {1}) : t1_space G :=
 ⟨assume x, by { convert is_closed_map_mul_right x _ h, simp }⟩
 
+@[priority 100, to_additive]
+instance topological_group.regular_space : regular_space G :=
+begin
+  refine regular_space.of_exists_mem_nhds_is_closed_subset (λ a s hs, _),
+  have : tendsto (λ p : G × G, p.1 * p.2) (𝓝 (a, 1)) (𝓝 a),
+    from continuous_mul.tendsto' _ _ (mul_one a),
+  rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩,
+  rw [← image_subset_iff, image_prod] at hUV,
+  refine ⟨closure U, mem_of_superset hU subset_closure, is_closed_closure, _⟩,
+  calc closure U ⊆ closure U * interior V : subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
+             ... = U * interior V         : is_open_interior.closure_mul U
+             ... ⊆ U * V                  : mul_subset_mul_left interior_subset
+             ... ⊆ s                      : hUV
+end
+
 @[to_additive]
-lemma topological_group.t3_space [t1_space G] : t3_space G :=
-⟨assume s a hs ha,
- let f := λ p : G × G, p.1 * (p.2)⁻¹ in
- have hf : continuous f := continuous_fst.mul continuous_snd.inv,
- -- a ∈ -s implies f (a, 1) ∈ -s, and so (a, 1) ∈ f⁻¹' (-s);
- -- and so can find t₁ t₂ open such that a ∈ t₁ × t₂ ⊆ f⁻¹' (-s)
- let ⟨t₁, t₂, ht₁, ht₂, a_mem_t₁, one_mem_t₂, t_subset⟩ :=
-   is_open_prod_iff.1 ((is_open_compl_iff.2 hs).preimage hf) a (1:G) (by simpa [f]) in
- begin
-   use [s * t₂, ht₂.mul_left, λ x hx, ⟨x, 1, hx, one_mem_t₂, mul_one _⟩],
-   rw [nhds_within, inf_principal_eq_bot, mem_nhds_iff],
-   refine ⟨t₁, _, ht₁, a_mem_t₁⟩,
-   rintros x hx ⟨y, z, hy, hz, yz⟩,
-   have : x * z⁻¹ ∈ sᶜ := (prod_subset_iff.1 t_subset) x hx z hz,
-   have : x * z⁻¹ ∈ s, rw ← yz, simpa,
-   contradiction
- end⟩
+lemma topological_group.t3_space [t1_space G] : t3_space G := ⟨⟩
 
 @[to_additive]
 lemma topological_group.t2_space [t1_space G] : t2_space G :=
-@t3_space.t2_space G _ (topological_group.t3_space G)
+by { haveI := topological_group.t3_space G, apply_instance }
 
 variables {G} (S : subgroup G) [subgroup.normal S] [is_closed (S : set G)]
 

src/topology/algebra/infinite_sum.lean

@@ -369,7 +369,7 @@ lemma summable.even_add_odd {f : ℕ → α} (he : summable (λ k, f (2 * k)))
   summable f :=
 (he.has_sum.even_add_odd ho.has_sum).summable
 
-lemma has_sum.sigma [t3_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
+lemma has_sum.sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
   (ha : has_sum f a) (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) : has_sum g a :=
 begin
   refine (at_top_basis.tendsto_iff (closed_nhds_basis a)).mpr _,
@@ -390,12 +390,12 @@ end
 
 /-- If a series `f` on `β × γ` has sum `a` and for each `b` the restriction of `f` to `{b} × γ`
 has sum `g b`, then the series `g` has sum `a`. -/
-lemma has_sum.prod_fiberwise [t3_space α] {f : β × γ → α} {g : β → α} {a : α}
+lemma has_sum.prod_fiberwise [regular_space α] {f : β × γ → α} {g : β → α} {a : α}
   (ha : has_sum f a) (hf : ∀b, has_sum (λc, f (b, c)) (g b)) :
   has_sum g a :=
 has_sum.sigma ((equiv.sigma_equiv_prod β γ).has_sum_iff.2 ha) hf
 
-lemma summable.sigma' [t3_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
+lemma summable.sigma' [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
   (ha : summable f) (hf : ∀b, summable (λc, f ⟨b, c⟩)) :
   summable (λb, ∑'c, f ⟨b, c⟩) :=
 (ha.has_sum.sigma (assume b, (hf b).has_sum)).summable
@@ -541,22 +541,22 @@ lemma tsum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (
   ∑'b, ∑ i in s, f i b = ∑ i in s, ∑'b, f i b :=
 (has_sum_sum $ assume i hi, (hf i hi).has_sum).tsum_eq
 
-lemma tsum_sigma' [t3_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
-  (h₁ : ∀b, summable (λc, f ⟨b, c⟩)) (h₂ : summable f) : ∑'p, f p = ∑'b c, f ⟨b, c⟩ :=
+variables [add_comm_monoid δ] [topological_space δ] [t3_space δ] [has_continuous_add δ]
+
+lemma tsum_sigma' {γ : β → Type*} {f : (Σb:β, γ b) → δ} (h₁ : ∀b, summable (λc, f ⟨b, c⟩))
+  (h₂ : summable f) : ∑'p, f p = ∑'b c, f ⟨b, c⟩ :=
 (h₂.has_sum.sigma (assume b, (h₁ b).has_sum)).tsum_eq.symm
 
-lemma tsum_prod' [t3_space α] {f : β × γ → α} (h : summable f)
-  (h₁ : ∀b, summable (λc, f (b, c))) :
+lemma tsum_prod' {f : β × γ → δ} (h : summable f) (h₁ : ∀b, summable (λc, f (b, c))) :
   ∑'p, f p = ∑'b c, f (b, c) :=
 (h.has_sum.prod_fiberwise (assume b, (h₁ b).has_sum)).tsum_eq.symm
 
-lemma tsum_comm' [t3_space α] {f : β → γ → α} (h : summable (function.uncurry f))
-  (h₁ : ∀b, summable (f b)) (h₂ : ∀ c, summable (λ b, f b c)) :
+lemma tsum_comm' {f : β → γ → δ} (h : summable (function.uncurry f)) (h₁ : ∀b, summable (f b))
+  (h₂ : ∀ c, summable (λ b, f b c)) :
   ∑' c b, f b c = ∑' b c, f b c :=
 begin
-  erw [← tsum_prod' h h₁, ← tsum_prod' h.prod_symm h₂, ← (equiv.prod_comm β γ).tsum_eq],
-  refl,
-  assumption
+  erw [← tsum_prod' h h₁, ← tsum_prod' h.prod_symm h₂, ← (equiv.prod_comm γ β).tsum_eq (uncurry f)],
+  refl
 end
 
 end has_continuous_add
@@ -1228,12 +1228,12 @@ local attribute [instance] topological_add_group.t3_space
 
 /-- The sum over the complement of a finset tends to `0` when the finset grows to cover the whole
 space. This does not need a summability assumption, as otherwise all sums are zero. -/
-lemma tendsto_tsum_compl_at_top_zero [t1_space α] (f : β → α) :
+lemma tendsto_tsum_compl_at_top_zero (f : β → α) :
   tendsto (λ (s : finset β), ∑' b : {x // x ∉ s}, f b) at_top (𝓝 0) :=
 begin
   by_cases H : summable f,
   { assume e he,
-    rcases nhds_is_closed he with ⟨o, ho, oe, o_closed⟩,
+    rcases exists_mem_nhds_is_closed_subset he with ⟨o, ho, o_closed, oe⟩,
     simp only [le_eq_subset, set.mem_preimage, mem_at_top_sets, filter.mem_map, ge_iff_le],
     obtain ⟨s, hs⟩ : ∃ (s : finset β), ∀ (t : finset β), disjoint t s → ∑ (b : β) in t, f b ∈ o :=
       cauchy_seq_finset_iff_vanishing.1 (tendsto.cauchy_seq H.has_sum) o ho,
@@ -1302,7 +1302,7 @@ lemma summable.sigma_factor {γ : β → Type*} {f : (Σb:β, γ b) → α}
   (ha : summable f) (b : β) : summable (λc, f ⟨b, c⟩) :=
 ha.comp_injective sigma_mk_injective
 
-lemma summable.sigma [t1_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
+lemma summable.sigma {γ : β → Type*} {f : (Σb:β, γ b) → α}
   (ha : summable f) : summable (λb, ∑'c, f ⟨b, c⟩) :=
 ha.sigma' (λ b, ha.sigma_factor b)
 

src/topology/algebra/order/basic.lean

@@ -1122,13 +1122,9 @@ lemma dense_iff_exists_between [densely_ordered α] [nontrivial α] {s : set α}
 
 @[priority 100] -- see Note [lower instance priority]
 instance order_topology.t3_space : t3_space α :=
-begin
-  refine ⟨λ s a hs ha, _⟩,
-  have : sᶜ ∈ 𝓝 a, from hs.is_open_compl.mem_nhds ha,
-  rcases exists_Icc_mem_subset_of_mem_nhds this with ⟨b, c, -, hmem, hsub⟩,
-  refine ⟨(Icc b c)ᶜ, is_closed_Icc.is_open_compl, subset_compl_comm.2 hsub, _⟩,
-  rwa [nhds_within, inf_principal_eq_bot, compl_compl]
-end
+{ to_regular_space := regular_space.of_exists_mem_nhds_is_closed_subset $
+    λ a s hs, let ⟨b, c, ha, hmem, hs⟩ := exists_Icc_mem_subset_of_mem_nhds hs
+      in ⟨Icc b c, hmem, is_closed_Icc, hs⟩ }
 
 /-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`,
 provided `a` is neither a bottom element nor a top element. -/

src/topology/algebra/order/extend_from.lean

@@ -17,7 +17,7 @@ universes u v
 variables {α : Type u} {β : Type v}
 
 lemma continuous_on_Icc_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
-  [order_topology α] [topological_space β] [t3_space β] {f : α → β} {a b : α}
+  [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α}
   {la lb : β} (hab : a ≠ b) (hf : continuous_on f (Ioo a b))
   (ha : tendsto f (𝓝[>] a) (𝓝 la)) (hb : tendsto f (𝓝[<] b) (𝓝 lb)) :
   continuous_on (extend_from (Ioo a b) f) (Icc a b) :=
@@ -55,7 +55,7 @@ end
 
 lemma continuous_on_Ico_extend_from_Ioo [topological_space α]
   [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
-  [t3_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  [regular_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
   (ha : tendsto f (𝓝[>] a) (𝓝 la)) :
   continuous_on (extend_from (Ioo a b) f) (Ico a b) :=
 begin
@@ -70,7 +70,7 @@ end
 
 lemma continuous_on_Ioc_extend_from_Ioo [topological_space α]
   [linear_order α] [densely_ordered α] [order_topology α] [topological_space β]
-  [t3_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  [regular_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
   (hb : tendsto f (𝓝[<] b) (𝓝 lb)) :
   continuous_on (extend_from (Ioo a b) f) (Ioc a b) :=
 begin

src/topology/algebra/with_zero_topology.lean

@@ -147,14 +147,14 @@ instance order_closed_topology : order_closed_topology Γ₀ :=
 /-- The topology on a linearly ordered group with zero element adjoined is T₃. -/
 @[priority 100]
 instance t3_space : t3_space Γ₀ :=
-t3_space.of_lift'_closure $ λ γ,
-  begin
-    rcases ne_or_eq γ 0 with h₀|rfl,
-    { rw [nhds_of_ne_zero h₀, lift'_pure (monotone_closure Γ₀), closure_singleton,
-        principal_singleton] },
-    { exact has_basis_nhds_zero.lift'_closure_eq_self
-      (λ x hx, is_closed_iff.2 $ or.inl $ zero_lt_iff.2 hx) },
-  end
+{ to_regular_space := regular_space.of_lift'_closure $ λ γ,
+    begin
+      rcases ne_or_eq γ 0 with h₀|rfl,
+      { rw [nhds_of_ne_zero h₀, lift'_pure (monotone_closure Γ₀), closure_singleton,
+          principal_singleton] },
+      { exact has_basis_nhds_zero.lift'_closure_eq_self
+        (λ x hx, is_closed_iff.2 $ or.inl $ zero_lt_iff.2 hx) },
+    end }
 
 /-- The topology on a linearly ordered group with zero element adjoined makes it a topological
 monoid. -/

src/topology/dense_embedding.lean

@@ -348,13 +348,13 @@ begin
   rw filter.has_basis_iff at h ⊢,
   intros T,
   refine ⟨λ hT, _, λ hT, _⟩,
-  { obtain ⟨T', hT₁, hT₂, hT₃⟩ := nhds_is_closed hT,
+  { obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_is_closed_subset hT,
     have hT₄ : f⁻¹' T' ∈ 𝓝 x,
     { rw hf.to_inducing.nhds_eq_comap x,
       exact ⟨T', hT₁, subset.rfl⟩, },
     obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄,
     exact ⟨i, hi, (closure_mono (image_subset f hi')).trans (subset.trans (closure_minimal
-      (image_subset_iff.mpr subset.rfl) hT₃) hT₂)⟩, },
+      (image_subset_iff.mpr subset.rfl) hT₂) hT₃)⟩, },
   { obtain ⟨i, hi, hi'⟩ := hT,
     suffices : closure (f '' s i) ∈ 𝓝 (f x), { filter_upwards [this] using hi', },
     replace h := (h (s i)).mpr ⟨i, hi, subset.rfl⟩,

src/topology/extend_from.lean

@@ -54,7 +54,7 @@ lemma extend_from_extends [t2_space Y] {f : X → Y} {A : set X} (hf : continuou
 
 /-- If `f` is a function to a T₃ space `Y` which has a limit within `A` at any
 point of a set `B ⊆ closure A`, then `extend_from A f` is continuous on `B`. -/
-lemma continuous_on_extend_from [t3_space Y] {f : X → Y} {A B : set X} (hB : B ⊆ closure A)
+lemma continuous_on_extend_from [regular_space Y] {f : X → Y} {A B : set X} (hB : B ⊆ closure A)
   (hf : ∀ x ∈ B, ∃ y, tendsto f (𝓝[A] x) (𝓝 y)) : continuous_on (extend_from A f) B :=
 begin
   set φ := extend_from A f,
@@ -79,7 +79,7 @@ end
 
 /-- If a function `f` to a T₃ space `Y` has a limit within a
 dense set `A` for any `x`, then `extend_from A f` is continuous. -/
-lemma continuous_extend_from [t3_space Y] {f : X → Y} {A : set X} (hA : dense A)
+lemma continuous_extend_from [regular_space Y] {f : X → Y} {A : set X} (hA : dense A)
   (hf : ∀ x, ∃ y, tendsto f (𝓝[A] x) (𝓝 y)) : continuous (extend_from A f) :=
 begin
   rw continuous_iff_continuous_on_univ,

src/topology/inseparable.lean

@@ -121,6 +121,11 @@ lemma specializes_iff_closure_subset :
 
 alias specializes_iff_closure_subset ↔ specializes.closure_subset _
 
+lemma filter.has_basis.specializes_iff {ι} {p : ι → Prop} {s : ι → set X}
+  (h : (𝓝 y).has_basis p s) :
+  x ⤳ y ↔ ∀ i, p i → x ∈ s i :=
+specializes_iff_pure.trans h.ge_iff
+
 lemma specializes_rfl : x ⤳ x := le_rfl
 
 @[refl] lemma specializes_refl (x : X) : x ⤳ x := specializes_rfl

src/topology/order.lean

@@ -226,6 +226,13 @@ instance : has_le (topological_space α) :=
 protected lemma topological_space.le_def {α} {t s : topological_space α} :
   t ≤ s ↔ s.is_open ≤ t.is_open := iff.rfl
 
+lemma is_open.mono {α} {t₁ t₂ : topological_space α} {s : set α} (hs : @is_open α t₂ s)
+  (h : t₁ ≤ t₂) : @is_open α t₁ s := h s hs
+
+lemma is_closed.mono {α} {t₁ t₂ : topological_space α} {s : set α} (hs : @is_closed α t₂ s)
+  (h : t₁ ≤ t₂) : @is_closed α t₁ s :=
+(@is_open_compl_iff α t₁ s).mp $ hs.is_open_compl.mono h
+
 /-- The ordering on topologies on the type `α`.
   `t ≤ s` if every set open in `s` is also open in `t` (`t` is finer than `s`). -/
 instance : partial_order (topological_space α) :=