feat: Port Topology.ContinuousFunction.T0Sierpinski (#2240)

Comments update and reflow only.

Mathlib.lean

@@ -1060,6 +1060,7 @@ import Mathlib.Topology.Connected
 import Mathlib.Topology.Constructions
 import Mathlib.Topology.ContinuousFunction.Basic
 import Mathlib.Topology.ContinuousFunction.CocompactMap
+import Mathlib.Topology.ContinuousFunction.T0Sierpinski
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Topology.DenseEmbedding
 import Mathlib.Topology.DiscreteQuotient

Mathlib/Topology/ContinuousFunction/T0Sierpinski.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2022 Ivan Sadofschi Costa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ivan Sadofschi Costa
+
+! This file was ported from Lean 3 source module topology.continuous_function.t0_sierpinski
+! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Order
+import Mathlib.Topology.Sets.Opens
+import Mathlib.Topology.ContinuousFunction.Basic
+
+/-!
+# Any T0 space embeds in a product of copies of the Sierpinski space.
+
+We consider `Prop` with the Sierpinski topology. If `X` is a topological space, there is a
+continuous map `productOfMemOpens` from `X` to `Opens X → Prop` which is the product of the maps
+`X → Prop` given by `x ↦ x ∈ u`.
+
+The map `productOfMemOpens` is always inducing. Whenever `X` is T0, `productOfMemOpens` is
+also injective and therefore an embedding.
+-/
+
+
+noncomputable section
+
+namespace TopologicalSpace
+
+theorem eq_induced_by_maps_to_sierpinski (X : Type _) [t : TopologicalSpace X] :
+    t = ⨅ u : Opens X, sierpinskiSpace.induced (· ∈ u) := by
+  apply le_antisymm
+  · rw [le_infᵢ_iff]
+    exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)
+  · intro u h
+    rw [← generateFrom_unionᵢ_isOpen]
+    apply isOpen_generateFrom_of_mem
+    simp only [Set.mem_unionᵢ, Set.mem_setOf_eq, isOpen_induced_iff]
+    exact ⟨⟨u, h⟩, {True}, isOpen_singleton_true, by simp [Set.preimage]⟩
+#align topological_space.eq_induced_by_maps_to_sierpinski TopologicalSpace.eq_induced_by_maps_to_sierpinski
+
+variable (X : Type _) [TopologicalSpace X]
+
+/-- The continuous map from `X` to the product of copies of the Sierpinski space, (one copy for each
+open subset `u` of `X`). The `u` coordinate of `productOfMemOpens x` is given by `x ∈ u`.
+-/
+def productOfMemOpens : C(X, Opens X → Prop) where
+  toFun x u := x ∈ u
+  continuous_toFun := continuous_pi_iff.2 fun u => continuous_Prop.2 u.isOpen
+#align topological_space.product_of_mem_opens TopologicalSpace.productOfMemOpens
+
+theorem productOfMemOpens_inducing : Inducing (productOfMemOpens X) := by
+  convert inducing_infᵢ_to_pi fun (u : Opens X) (x : X) => x ∈ u
+  apply eq_induced_by_maps_to_sierpinski
+#align topological_space.product_of_mem_opens_inducing TopologicalSpace.productOfMemOpens_inducing
+
+theorem productOfMemOpens_injective [T0Space X] : Function.Injective (productOfMemOpens X) := by
+  intro x1 x2 h
+  apply Inseparable.eq
+  rw [← Inducing.inseparable_iff (productOfMemOpens_inducing X), h]
+#align topological_space.product_of_mem_opens_injective TopologicalSpace.productOfMemOpens_injective
+
+theorem productOfMemOpens_embedding [T0Space X] : Embedding (productOfMemOpens X) :=
+  Embedding.mk (productOfMemOpens_inducing X) (productOfMemOpens_injective X)
+#align topological_space.product_of_mem_opens_embedding TopologicalSpace.productOfMemOpens_embedding
+
+end TopologicalSpace
+