feat(topological/homeomorph): the image of a set (#7147)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/data/equiv/basic.lean

@@ -1461,6 +1461,18 @@ dif_pos h
 
 end subtype_equiv_codomain
 
+/--
+A set is equivalent to its image under an equivalence.
+-/
+-- We could construct this using `equiv.set.image e s e.injective`,
+-- but this definition provides an explicit inverse.
+@[simps]
+def image {α β : Type*} (e : α ≃ β) (s : set α) : s ≃ e '' s :=
+{ to_fun := λ x, ⟨e x.1, by simp⟩,
+  inv_fun := λ y, ⟨e.symm y.1, by { rcases y with ⟨-, ⟨a, ⟨m, rfl⟩⟩⟩, simpa using m, }⟩,
+  left_inv := λ x, by simp,
+  right_inv := λ y, by simp, }.
+
 namespace set
 open set
 

src/topology/homeomorph.lean

@@ -65,6 +65,9 @@ rfl
 @[continuity]
 protected lemma continuous (h : α ≃ₜ β) : continuous h := h.continuous_to_fun
 
+@[continuity] -- otherwise `by continuity` can't prove continuity of `h.to_equiv.symm`
+protected lemma continuous_symm (h : α ≃ₜ β) : continuous (h.symm) := h.continuous_inv_fun
+
 @[simp] lemma apply_symm_apply (h : α ≃ₜ β) (x : β) : h (h.symm x) = x :=
 h.to_equiv.apply_symm_apply x
 
@@ -311,4 +314,12 @@ homeomorph_of_continuous_open (equiv.sigma_prod_distrib σ β).symm
 
 end distrib
 
+/--
+A subset of a topological space is homeomorphic to its image under a homeomorphism.
+-/
+def image (e : α ≃ₜ β) (s : set α) : s ≃ₜ e '' s :=
+{ continuous_to_fun := by continuity!,
+  continuous_inv_fun := by continuity!,
+  ..e.to_equiv.image s, }
+
 end homeomorph