feat: two topology lemmas (#9624)

grunweg · grunweg · commit c532ace05243 · 2024-01-11T11:03:27.000Z
From sphere-eversion; I'm just upstreaming it. Co-authored-by: @fpvandoorn
diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean
@@ -929,6 +929,15 @@ theorem Inducing.isCompact_preimage {f : X → Y} (hf : Inducing f) (hf' : IsClo
   replace hK := hK.inter_right hf'
   rwa [hf.isCompact_iff, image_preimage_eq_inter_range]
 
+lemma Inducing.isCompact_preimage_iff {f : X → Y} (hf : Inducing f) {K : Set Y}
+    (Kf : K ⊆ range f) : IsCompact (f ⁻¹' K) ↔ IsCompact K := by
+  rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]
+
+/-- The preimage of a compact set in the image of an inducing map is compact. -/
+lemma Inducing.isCompact_preimage' {f : X → Y} (hf : Inducing f) {K : Set Y}
+    (hK: IsCompact K) (Kf : K ⊆ range f) : IsCompact (f ⁻¹' K) :=
+  (hf.isCompact_preimage_iff Kf).2 hK
+
 /-- The preimage of a compact set under a closed embedding is a compact set. -/
 theorem ClosedEmbedding.isCompact_preimage {f : X → Y} (hf : ClosedEmbedding f)
     {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K) :=
