feat(Topology/Sets): injectivity of Compacts.map (#31381)

Author: gasparattila

Mathlib/Topology/Sets/Compacts.lean

@@ -148,10 +148,21 @@ theorem map_comp (f : β → γ) (g : α → β) (hf : Continuous f) (hg : Conti
     K.map (f ∘ g) (hf.comp hg) = (K.map g hg).map f hf :=
   Compacts.ext <| Set.image_comp _ _ _
 
+theorem map_injective {f : α → β} (hf : Continuous f) (hf' : Function.Injective f) :
+    Function.Injective (Compacts.map f hf) :=
+  .of_comp (f := SetLike.coe) <| hf'.image_injective.comp SetLike.coe_injective
+
 @[simp]
 theorem map_singleton {f : α → β} (hf : Continuous f) (x : α) : Compacts.map f hf {x} = {f x} :=
   Compacts.ext Set.image_singleton
 
+@[simp]
+theorem map_injective_iff {f : α → β} (hf : Continuous f) :
+    Function.Injective (Compacts.map f hf) ↔ Function.Injective f := by
+  refine ⟨fun h => .of_comp (f := ({·} : β → Compacts β)) ?_, map_injective hf⟩
+  simp_rw [Function.comp_def, ← map_singleton hf]
+  exact h.comp singleton_injective
+
 /-- A homeomorphism induces an equivalence on compact sets, by taking the image. -/
 @[simps]
 protected def equiv (f : α ≃ₜ β) : Compacts α ≃ Compacts β where