feat: add DiscreteTopology.of_continuous_injective (#7029)

leanprover-community · Sep 8, 2023 · bb3c2eb · bb3c2eb
1 parent 2df6bb4
commit bb3c2eb
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 6 deletions.
diff --git a/Mathlib/Topology/Maps.lean b/Mathlib/Topology/Maps.lean
@@ -256,13 +256,13 @@ theorem Embedding.closure_eq_preimage_closure_image {e : α → β} (he : Embedd
   he.1.closure_eq_preimage_closure_image s
 #align embedding.closure_eq_preimage_closure_image Embedding.closure_eq_preimage_closure_image
 
-/-- The topology induced under an inclusion `f : X → Y` from the discrete topological space `Y`
-is the discrete topology on `X`. -/
-theorem Embedding.discreteTopology {X Y : Type*} [TopologicalSpace X] [tY : TopologicalSpace Y]
+/-- The topology induced under an inclusion `f : X → Y` from a discrete topological space `Y`
+is the discrete topology on `X`.
+
+See also `DiscreteTopology.of_continuous_injective`. -/
+theorem Embedding.discreteTopology {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
     [DiscreteTopology Y] {f : X → Y} (hf : Embedding f) : DiscreteTopology X :=
-  discreteTopology_iff_nhds.2 fun x => by
-    rw [hf.nhds_eq_comap, nhds_discrete, comap_pure, ← image_singleton, hf.inj.preimage_image,
-      principal_singleton]
+  .of_continuous_injective hf.continuous hf.inj
 #align embedding.discrete_topology Embedding.discreteTopology
 
 end Embedding

diff --git a/Mathlib/Topology/Order.lean b/Mathlib/Topology/Order.lean
@@ -359,6 +359,15 @@ theorem discreteTopology_iff_nhds_ne [TopologicalSpace α] :
   simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]
 #align discrete_topology_iff_nhds_ne discreteTopology_iff_nhds_ne
 
+/-- If the codomain of a continuous injective function has discrete topology,
+then so does the domain.
+
+See also `Embedding.discreteTopology` for an important special case. -/
+theorem DiscreteTopology.of_continuous_injective
+    {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β}
+    (hc : Continuous f) (hinj : Injective f) : DiscreteTopology α :=
+  forall_open_iff_discrete.1 fun s ↦ hinj.preimage_image s ▸ (isOpen_discrete _).preimage hc
+
 end Lattice
 
 section GaloisConnection