doc(Topology/Homeomorph): two docstrings (#7595)

leanprover-community · Oct 10, 2023 · 10922d6 · 10922d6
1 parent 201c8ee
commit 10922d6
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
@@ -258,11 +258,13 @@ protected theorem secondCountableTopology [TopologicalSpace.SecondCountableTopol
   h.inducing.secondCountableTopology
 #align homeomorph.second_countable_topology Homeomorph.secondCountableTopology
 
+/-- If `h : α → β` is a homeomorphism, `h(s)` is compact iff `s` is. -/
 @[simp]
 theorem isCompact_image {s : Set α} (h : α ≃ₜ β) : IsCompact (h '' s) ↔ IsCompact s :=
   h.embedding.isCompact_iff_isCompact_image.symm
 #align homeomorph.is_compact_image Homeomorph.isCompact_image
 
+/-- If `h : α → β` is a homeomorphism, `h⁻¹(s)` is compact iff `s` is. -/
 @[simp]
 theorem isCompact_preimage {s : Set β} (h : α ≃ₜ β) : IsCompact (h ⁻¹' s) ↔ IsCompact s := by
   rw [← image_symm]; exact h.symm.isCompact_image