feat(topology/separation): t0_space and t1_space for α × β and …

…`Π i, α i` (#14418)

src/analysis/normed_space/pi_Lp.lean

@@ -206,9 +206,7 @@ instance [Π i, pseudo_emetric_space (β i)] : pseudo_emetric_space (pi_Lp p β)
 /-- emetric space instance on the product of finitely many emetric spaces, using the `L^p`
 edistance, and having as uniformity the product uniformity. -/
 instance [Π i, emetric_space (α i)] : emetric_space (pi_Lp p α) :=
-@emetric.of_t0_pseudo_emetric_space _ _ $
-  -- TODO: add `Pi.t0_space`
-  by { haveI : t2_space (pi_Lp p α) := Pi.t2_space, apply_instance }
+@emetric.of_t0_pseudo_emetric_space (pi_Lp p α) _ pi.t0_space
 
 variables {p β}
 lemma edist_eq [Π i, pseudo_emetric_space (β i)] (x y : pi_Lp p β) :

src/data/set/prod.lean

@@ -350,6 +350,9 @@ by { ext, simp [pi] }
 
 lemma singleton_pi' (i : ι) (t : Π i, set (α i)) : pi {i} t = {x | x i ∈ t i} := singleton_pi i t
 
+lemma univ_pi_singleton (f : Π i, α i) : pi univ (λ i, {f i}) = ({f} : set (Π i, α i)) :=
+ext $ λ g, by simp [funext_iff]
+
 lemma pi_if {p : ι → Prop} [h : decidable_pred p] (s : set ι) (t₁ t₂ : Π i, set (α i)) :
   pi s (λ i, if p i then t₁ i else t₂ i) = pi {i ∈ s | p i} t₁ ∩ pi {i ∈ s | ¬ p i} t₂ :=
 begin

src/topology/separation.lean

@@ -176,6 +176,11 @@ lemma indistinguishable_iff_nhds_eq {x y : α} : indistinguishable x y ↔ 𝓝
 
 alias indistinguishable_iff_nhds_eq ↔ indistinguishable.nhds_eq _
 
+lemma indistinguishable.map [topological_space β] {x y : α} {f : α → β}
+  (h : indistinguishable x y) (hf : continuous f) :
+  indistinguishable (f x) (f y) :=
+λ U hU, h (f ⁻¹' U) (hU.preimage hf)
+
 lemma t0_space_iff_distinguishable (α : Type u) [topological_space α] :
   t0_space α ↔ ∀ (x y : α), x ≠ y → ¬ indistinguishable x y :=
 begin
@@ -185,6 +190,10 @@ begin
   simp_rw xor_iff_not_iff,
 end
 
+lemma t0_space_iff_indistinguishable (α : Type u) [topological_space α] :
+  t0_space α ↔ ∀ (x y : α), indistinguishable x y → x = y :=
+(t0_space_iff_distinguishable α).trans $ forall₂_congr $ λ a b, not_imp_not
+
 @[simp] lemma nhds_eq_nhds_iff [t0_space α] {a b : α} : 𝓝 a = 𝓝 b ↔ a = b :=
 function.injective.eq_iff $ λ x y h, of_not_not $
   λ hne, (t0_space_iff_distinguishable α).mp ‹_› x y hne (indistinguishable_iff_nhds_eq.mpr h)
@@ -288,19 +297,16 @@ instance subtype.t0_space [t0_space α] {p : α → Prop} : t0_space (subtype p)
 embedding_subtype_coe.t0_space
 
 theorem t0_space_iff_or_not_mem_closure (α : Type u) [topological_space α] :
-  t0_space α ↔ (∀ a b : α, (a ≠ b) → (a ∉ closure ({b} : set α) ∨ b ∉ closure ({a} : set α))) :=
-begin
-  simp only [← not_and_distrib, t0_space_def, not_and],
-  refine forall₃_congr (λ a b _, ⟨_, λ h, _⟩),
-  { rintro ⟨s, h₁, (⟨h₂, h₃ : b ∈ sᶜ⟩|⟨h₂, h₃ : a ∈ sᶜ⟩)⟩ ha hb; rw ← is_closed_compl_iff at h₁,
-    { exact (is_closed.closure_subset_iff h₁).mpr (set.singleton_subset_iff.mpr h₃) ha h₂ },
-    { exact (is_closed.closure_subset_iff h₁).mpr (set.singleton_subset_iff.mpr h₃) hb h₂ } },
-  { by_cases h' : a ∈ closure ({b} : set α),
-    { exact ⟨(closure {a})ᶜ, is_closed_closure.1,
-        or.inr ⟨h h', not_not.mpr (subset_closure (set.mem_singleton a))⟩⟩ },
-    { exact ⟨(closure {b})ᶜ, is_closed_closure.1,
-        or.inl ⟨h', not_not.mpr (subset_closure (set.mem_singleton b))⟩⟩ } }
-end
+  t0_space α ↔ (∀ a b : α, a ≠ b → (a ∉ closure ({b} : set α) ∨ b ∉ closure ({a} : set α))) :=
+by simp only [t0_space_iff_distinguishable, indistinguishable_iff_closure, not_and_distrib]
+
+instance [topological_space β] [t0_space α] [t0_space β] : t0_space (α × β) :=
+(t0_space_iff_indistinguishable _).2 $
+  λ x y h, prod.ext (h.map continuous_fst).eq (h.map continuous_snd).eq
+
+instance {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)] [Π i, t0_space (π i)] :
+  t0_space (Π i, π i) :=
+(t0_space_iff_indistinguishable _).2 $ λ x y h, funext $ λ i, (h.map (continuous_apply i)).eq
 
 /-- A T₁ space, also known as a Fréchet space, is a topological space
   where every singleton set is closed. Equivalently, for every pair
@@ -477,6 +483,13 @@ instance subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p
   t1_space (subtype p) :=
 embedding_subtype_coe.t1_space
 
+instance [topological_space β] [t1_space α] [t1_space β] : t1_space (α × β) :=
+⟨λ ⟨a, b⟩, @singleton_prod_singleton _ _ a b ▸ is_closed_singleton.prod is_closed_singleton⟩
+
+instance {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)] [Π i, t1_space (π i)] :
+  t1_space (Π i, π i) :=
+⟨λ f, univ_pi_singleton f ▸ is_closed_set_pi (λ i hi, is_closed_singleton)⟩
+
 @[priority 100] -- see Note [lower instance priority]
 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⟩⟩⟩
@@ -501,9 +514,7 @@ hs.induction_on (by simp) $ λ x, by simp
 
 lemma is_closed_map_const {α β} [topological_space α] [topological_space β] [t1_space β] {y : β} :
   is_closed_map (function.const α y) :=
-begin
-  apply is_closed_map.of_nonempty, intros s hs h2s, simp_rw [h2s.image_const, is_closed_singleton]
-end
+is_closed_map.of_nonempty $ λ s hs h2s, by simp_rw [h2s.image_const, is_closed_singleton]
 
 lemma bInter_basis_nhds [t1_space α] {ι : Sort*} {p : ι → Prop} {s : ι → set α} {x : α}
   (h : (𝓝 x).has_basis p s) : (⋂ i (h : p i), s i) = {x} :=