English
A set is equivalent to its image under an equivalence: the restriction of the equivalence to the set yields a bijection between the set and its image.
Русский
Множество эквивалентно своему образу под эквивалентностью: ограничение эквивалентности на множество дает биекцию между множеством и его образом.
LaTeX
$$$ s \simeq e''s $$$
Lean4
/-- A set is equivalent to its image under an equivalence.
-/
@[simps]
def image {α β : Type*} (e : α ≃ β) (s : Set α) : s ≃ e '' s
where
toFun x := ⟨e x.1, by simp⟩
invFun
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
