refactor(topology/separation): rename regular_space to t3_space (#…

…15169)

I'm going to add a version of `regular_space` without `t0_space` and prove, e.g., that any uniform space is a regular space in this sense. To do this, I need to rename the existing `regular_space`.

src/analysis/complex/upper_half_plane/topology.lean

@@ -37,8 +37,8 @@ lemma continuous_im : continuous im := complex.continuous_im.comp continuous_coe
 instance : topological_space.second_countable_topology ℍ :=
 topological_space.subtype.second_countable_topology _ _
 
-instance : regular_space ℍ := subtype.regular_space
-instance : normal_space ℍ := normal_space_of_regular_second_countable ℍ
+instance : t3_space ℍ := subtype.t3_space
+instance : normal_space ℍ := normal_space_of_t3_second_countable ℍ
 
 instance : contractible_space ℍ :=
 (convex_halfspace_im_gt 0).contractible_space ⟨I, one_pos.trans_eq I_im.symm⟩

src/analysis/locally_convex/balanced_core_hull.lean

@@ -247,7 +247,7 @@ end
 
 variables (𝕜 E)
 
-lemma nhds_basis_closed_balanced [regular_space E] : (𝓝 (0 : E)).has_basis
+lemma nhds_basis_closed_balanced [t3_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/analysis/locally_convex/bounded.lean

@@ -164,7 +164,7 @@ section uniform_add_group
 
 variables [nondiscrete_normed_field 𝕜] [add_comm_group E] [module 𝕜 E]
 variables [uniform_space E] [uniform_add_group E] [has_continuous_smul 𝕜 E]
-variables [regular_space E]
+variables [t3_space E]
 
 lemma totally_bounded.is_vonN_bounded {s : set E} (hs : totally_bounded s) :
   bornology.is_vonN_bounded 𝕜 s :=

src/topology/alexandroff.lean

@@ -350,7 +350,7 @@ by induction x using alexandroff.rec; induction y using alexandroff.rec;
 
 In this section we prove that `alexandroff X` is a compact space; it is a T₀ (resp., T₁) space if
 the original space satisfies the same separation axiom. If the original space is a locally compact
-Hausdorff space, then `alexandroff X` is a normal (hence, regular and Hausdorff) space.
+Hausdorff space, then `alexandroff X` is a normal (hence, T₃ and Hausdorff) space.
 
 Finally, if the original space `X` is *not* compact and is a preconnected space, then
 `alexandroff X` is a connected space.

src/topology/algebra/group.lean

@@ -969,7 +969,7 @@ 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 }⟩
 
 @[to_additive]
-lemma topological_group.regular_space [t1_space G] : regular_space G :=
+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,
@@ -989,15 +989,15 @@ lemma topological_group.regular_space [t1_space G] : regular_space G :=
 
 @[to_additive]
 lemma topological_group.t2_space [t1_space G] : t2_space G :=
-@regular_space.t2_space G _ (topological_group.regular_space G)
+@t3_space.t2_space G _ (topological_group.t3_space G)
 
 variables {G} (S : subgroup G) [subgroup.normal S] [is_closed (S : set G)]
 
 @[to_additive]
-instance subgroup.regular_quotient_of_is_closed
-  (S : subgroup G) [subgroup.normal S] [is_closed (S : set G)] : regular_space (G ⧸ S) :=
+instance subgroup.t3_quotient_of_is_closed
+  (S : subgroup G) [subgroup.normal S] [is_closed (S : set G)] : t3_space (G ⧸ S) :=
 begin
-  suffices : t1_space (G ⧸ S), { exact @topological_group.regular_space _ _ _ _ this, },
+  suffices : t1_space (G ⧸ S), { exact @topological_group.t3_space _ _ _ _ this, },
   have hS : is_closed (S : set G) := infer_instance,
   rw ← quotient_group.ker_mk S at hS,
   exact topological_group.t1_space (G ⧸ S) ((quotient_map_quotient_mk.is_closed_preimage).mp hS),

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 [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
+lemma has_sum.sigma [t3_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,17 +390,17 @@ 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 [regular_space α] {f : β × γ → α} {g : β → α} {a : α}
+lemma has_sum.prod_fiberwise [t3_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' [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
+lemma summable.sigma' [t3_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
 
-lemma has_sum.sigma_of_has_sum [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α}
+lemma has_sum.sigma_of_has_sum [t3_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α}
   {a : α} (ha : has_sum g a) (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) (hf' : summable f) :
   has_sum f a :=
 by simpa [(hf'.has_sum.sigma hf).unique ha] using hf'.has_sum
@@ -525,16 +525,16 @@ 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' [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
+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⟩ :=
 (h₂.has_sum.sigma (assume b, (h₁ b).has_sum)).tsum_eq.symm
 
-lemma tsum_prod' [regular_space α] {f : β × γ → α} (h : summable f)
+lemma tsum_prod' [t3_space α] {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' [regular_space α] {f : β → γ → α} (h : summable (function.uncurry f))
+lemma tsum_comm' [t3_space α] {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
@@ -1203,7 +1203,7 @@ begin
     exact hde _ (h _ finset.sdiff_disjoint) _ (h _ finset.sdiff_disjoint) }
 end
 
-local attribute [instance] topological_add_group.regular_space
+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. -/
@@ -1503,7 +1503,7 @@ We first establish results about arbitrary index types, `β` and `γ`, and then
 
 section tsum_mul_tsum
 
-variables [topological_space α] [regular_space α] [non_unital_non_assoc_semiring α]
+variables [topological_space α] [t3_space α] [non_unital_non_assoc_semiring α]
   [topological_semiring α] {f : β → α} {g : γ → α} {s t u : α}
 
 lemma has_sum.mul_eq (hf : has_sum f s) (hg : has_sum g t)
@@ -1556,7 +1556,7 @@ lemma summable_mul_prod_iff_summable_mul_sigma_antidiagonal {f g : ℕ → α} :
   summable (λ x : (Σ (n : ℕ), nat.antidiagonal n), f (x.2 : ℕ × ℕ).1 * g (x.2 : ℕ × ℕ).2) :=
 nat.sigma_antidiagonal_equiv_prod.summable_iff.symm
 
-variables [regular_space α] [topological_semiring α]
+variables [t3_space α] [topological_semiring α]
 
 lemma summable_sum_mul_antidiagonal_of_summable_mul {f g : ℕ → α}
   (h : summable (λ x : ℕ × ℕ, f x.1 * g x.2)) :

src/topology/algebra/module/basic.lean

@@ -2036,11 +2036,11 @@ begin
   exact continuous_quot_mk.comp continuous_smul
 end
 
-instance regular_quotient_of_is_closed [topological_add_group M] [is_closed (S : set M)] :
-  regular_space (M ⧸ S) :=
+instance t3_quotient_of_is_closed [topological_add_group M] [is_closed (S : set M)] :
+  t3_space (M ⧸ S) :=
 begin
   letI : is_closed (S.to_add_subgroup : set M) := ‹_›,
-  exact S.to_add_subgroup.regular_quotient_of_is_closed
+  exact S.to_add_subgroup.t3_quotient_of_is_closed
 end
 
 end submodule

src/topology/algebra/order/basic.lean

@@ -1083,7 +1083,7 @@ lemma dense_iff_exists_between [densely_ordered α] [nontrivial α] {s : set α}
 lemma order_topology.t2_space : t2_space α := by apply_instance
 
 @[priority 100] -- see Note [lower instance priority]
-instance order_topology.regular_space : regular_space α :=
+instance order_topology.t3_space : t3_space α :=
 { regular := assume s a hs ha,
     have hs' : sᶜ ∈ 𝓝 a, from is_open.mem_nhds hs.is_open_compl ha,
     have ∃t:set α, is_open t ∧ (∀l∈ s, l < a → l ∈ t) ∧ 𝓝[t] a = ⊥,

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 β] [regular_space β] {f : α → β} {a b : α}
+  [order_topology α] [topological_space β] [t3_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 β]
-  [regular_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  [t3_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 β]
-  [regular_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  [t3_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/uniform_field.lean

@@ -66,7 +66,7 @@ def hat_inv : hat K → hat K := dense_inducing_coe.extend (λ x : K, (coe x⁻
 lemma continuous_hat_inv [completable_top_field K] {x : hat K} (h : x ≠ 0) :
   continuous_at hat_inv x :=
 begin
-  haveI : regular_space (hat K) := completion.regular_space K,
+  haveI : t3_space (hat K) := completion.t3_space K,
   refine dense_inducing_coe.continuous_at_extend _,
   apply mem_of_superset (compl_singleton_mem_nhds h),
   intros y y_ne,

src/topology/algebra/valued_field.lean

@@ -283,7 +283,7 @@ end
 @[simp, norm_cast]
 lemma extension_extends (x : K) : extension (x : hat K) = v x :=
 begin
-  haveI : t2_space Γ₀ := regular_space.t2_space _,
+  haveI : t2_space Γ₀ := t3_space.t2_space _,
   refine completion.dense_inducing_coe.extend_eq_of_tendsto _,
   rw ← completion.dense_inducing_coe.nhds_eq_comap,
   exact valued.continuous_valuation.continuous_at,

src/topology/algebra/with_zero_topology.lean

@@ -18,7 +18,7 @@ In particular the topology is the following:
 `γ₀ ∈ Γ₀ such that {γ | γ < γ₀} ⊆ U`", but this fact is not proven here since the neighborhoods
 description is what is actually useful.
 
-We prove this topology is ordered and regular (in addition to be compatible with the monoid
+We prove this topology is ordered and T₃ (in addition to be compatible with the monoid
 structure).
 
 All this is useful to extend a valuation to a completion. This is an abstract version of how the
@@ -29,7 +29,7 @@ absolute value (resp. `p`-adic absolute value) on `ℚ` is extended to `ℝ` (re
 This topology is not defined as an instance since it may not be the desired topology on
 a linearly ordered commutative group with zero. You can locally activate this topology using
 `local attribute [instance] linear_ordered_comm_group_with_zero.topological_space`
-All other instances will (`ordered_topology`, `regular_space`, `has_continuous_mul`) then follow.
+All other instances will (`ordered_topology`, `t3_space`, `has_continuous_mul`) then follow.
 
 -/
 
@@ -209,9 +209,9 @@ instance ordered_topology : order_closed_topology Γ₀ :=
       rwa [h1, h2] }
   end }
 
-/-- The topology on a linearly ordered group with zero element adjoined is T₃ (aka regular). -/
+/-- The topology on a linearly ordered group with zero element adjoined is T₃. -/
 @[priority 100]
-instance regular_space : regular_space Γ₀ :=
+instance t3_space : t3_space Γ₀ :=
 begin
   haveI : t1_space Γ₀ := t2_space.t1_space,
   split,

src/topology/dense_embedding.lean

@@ -16,7 +16,7 @@ This file defines three properties of functions:
 * `dense_embedding e`  means `e` is also an `embedding`.
 
 The main theorem `continuous_extend` gives a criterion for a function
-`f : X → Z` to a regular (T₃) space Z to extend along a dense embedding
+`f : X → Z` to a T₃ space Z to extend along a dense embedding
 `i : X → Y` to a continuous function `g : Y → Z`. Actually `i` only
 has to be `dense_inducing` (not necessarily injective).
 
@@ -179,7 +179,7 @@ lemma extend_unique [t2_space γ] {f : α → γ} {g : β → γ} (di : dense_in
   di.extend f = g :=
 funext $ λ b, extend_unique_at di (eventually_of_forall hf) hg.continuous_at
 
-lemma continuous_at_extend [regular_space γ] {b : β} {f : α → γ} (di : dense_inducing i)
+lemma continuous_at_extend [t3_space γ] {b : β} {f : α → γ} (di : dense_inducing i)
   (hf : ∀ᶠ x in 𝓝 b, ∃c, tendsto f (comap i $ 𝓝 x) (𝓝 c)) :
   continuous_at (di.extend f) b :=
 begin
@@ -206,7 +206,7 @@ begin
   tauto,
 end
 
-lemma continuous_extend [regular_space γ] {f : α → γ} (di : dense_inducing i)
+lemma continuous_extend [t3_space γ] {f : α → γ} (di : dense_inducing i)
   (hf : ∀b, ∃c, tendsto f (comap i (𝓝 b)) (𝓝 c)) : continuous (di.extend f) :=
 continuous_iff_continuous_at.mpr $ assume b, di.continuous_at_extend $ univ_mem' hf
 
@@ -338,9 +338,9 @@ lemma dense_range.equalizer (hfd : dense_range f)
 funext $ λ y, hfd.induction_on y (is_closed_eq hg hh) $ congr_fun H
 end
 
--- Bourbaki GT III §3 no.4 Proposition 7 (generalised to any dense-inducing map to a regular space)
+-- Bourbaki GT III §3 no.4 Proposition 7 (generalised to any dense-inducing map to a T₃ space)
 lemma filter.has_basis.has_basis_of_dense_inducing
-  [topological_space α] [topological_space β] [regular_space β]
+  [topological_space α] [topological_space β] [t3_space β]
   {ι : Type*} {s : ι → set α} {p : ι → Prop} {x : α} (h : (𝓝 x).has_basis p s)
   {f : α → β} (hf : dense_inducing f) :
   (𝓝 (f x)).has_basis p $ λ i, closure $ f '' (s i) :=

src/topology/extend_from.lean

@@ -18,7 +18,7 @@ This is analoguous to the way `dense_inducing.extend` "extends" a function
 The main theorem we prove about this definition is `continuous_on_extend_from`
 which states that, for `extend_from A f` to be continuous on a set `B ⊆ closure A`,
 it suffices that `f` converges within `A` at any point of `B`, provided that
-`f` is a function to a regular space.
+`f` is a function to a T₃ space.
 
 -/
 
@@ -52,9 +52,9 @@ lemma extend_from_extends [t2_space Y] {f : X → Y} {A : set X} (hf : continuou
   ∀ x ∈ A, extend_from A f x = f x :=
 λ x x_in, extend_from_eq (subset_closure x_in) (hf x x_in)
 
-/-- If `f` is a function to a regular space `Y` which has a limit within `A` at any
+/-- 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 [regular_space Y] {f : X → Y} {A B : set X} (hB : B ⊆ closure A)
+lemma continuous_on_extend_from [t3_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,
@@ -77,9 +77,9 @@ begin
   exact V'_closed.mem_of_tendsto limy (mem_of_superset this hV)
 end
 
-/-- If a function `f` to a regular space `Y` has a limit within a
+/-- 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 [regular_space Y] {f : X → Y} {A : set X} (hA : dense A)
+lemma continuous_extend_from [t3_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/homeomorph.lean

@@ -196,8 +196,8 @@ h.symm.embedding.t1_space
 protected lemma t2_space [t2_space α] (h : α ≃ₜ β) : t2_space β :=
 h.symm.embedding.t2_space
 
-protected lemma regular_space [regular_space α] (h : α ≃ₜ β) : regular_space β :=
-h.symm.embedding.regular_space
+protected lemma t3_space [t3_space α] (h : α ≃ₜ β) : t3_space β :=
+h.symm.embedding.t3_space
 
 protected lemma dense_embedding (h : α ≃ₜ β) : dense_embedding h :=
 { dense   := h.surjective.dense_range,

src/topology/metric_space/metrizable.lean

@@ -7,12 +7,12 @@ import topology.urysohns_lemma
 import topology.continuous_function.bounded
 
 /-!
-# Metrizability of a regular topological space with second countable topology
+# Metrizability of a T₃ topological space with second countable topology
 
 In this file we define metrizable topological spaces, i.e., topological spaces for which there
 exists a metric space structure that generates the same topology.
 
-We also show that a regular topological space with second countable topology `X` is metrizable.
+We also show that a T₃ topological space with second countable topology `X` is metrizable.
 
 First we prove that `X` can be embedded into `l^∞`, then use this embedding to pull back the metric
 space structure.
@@ -119,13 +119,13 @@ embedding_subtype_coe.metrizable_space
 instance metrizable_space_pi [Π i, metrizable_space (π i)] : metrizable_space (Π i, π i) :=
 by { letI := λ i, metrizable_space_metric (π i), apply_instance }
 
-variables (X) [regular_space X] [second_countable_topology X]
+variables (X) [t3_space X] [second_countable_topology X]
 
-/-- A regular topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`.
+/-- A T₃ topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`.
 -/
 lemma exists_embedding_l_infty : ∃ f : X → (ℕ →ᵇ ℝ), embedding f :=
 begin
-  haveI : normal_space X := normal_space_of_regular_second_countable X,
+  haveI : normal_space X := normal_space_of_t3_second_countable X,
   -- Choose a countable basis, and consider the set `s` of pairs of set `(U, V)` such that `U ∈ B`,
   -- `V ∈ B`, and `closure U ⊆ V`.
   rcases exists_countable_basis X with ⟨B, hBc, -, hB⟩,
@@ -203,12 +203,12 @@ begin
     exacts [hy _ hle, (real.dist_le_of_mem_Icc (hf0ε _ _) (hf0ε _ _)).trans (by rwa sub_zero)] }
 end
 
-/-- *Urysohn's metrization theorem* (Tychonoff's version): a regular topological space with second
+/-- *Urysohn's metrization theorem* (Tychonoff's version): a T₃ topological space with second
 countable topology `X` is metrizable, i.e., there exists a metric space structure that generates the
 same topology. -/
-lemma metrizable_space_of_regular_second_countable : metrizable_space X :=
+lemma metrizable_space_of_t3_second_countable : metrizable_space X :=
 let ⟨f, hf⟩ := exists_embedding_l_infty X in hf.metrizable_space
 
-instance : metrizable_space ennreal := metrizable_space_of_regular_second_countable ennreal
+instance : metrizable_space ennreal := metrizable_space_of_t3_second_countable ennreal
 
 end topological_space