English
If S is a set of elements of range f, then the image under rangeSplitting f yields a bijection with S. There is a canonical equivalence rangeSplitting f '' S ≃ S.
Русский
Если S — множество элементов из образа f, то образ подстановки rangeSplitting f образует биекцию с S; существует каноническое соответствие rangeSplitting f '' S ≃ S.
LaTeX
$$$\\mathrm{rangeSplitting} f '' S \\cong S$$$
Lean4
/-- If `s` is a set in `range f`,
then its image under `rangeSplitting f` is in bijection (via `f`) with `s`.
-/
@[simps]
noncomputable def rangeSplittingImageEquiv {α β : Type*} (f : α → β) (s : Set (range f)) : rangeSplitting f '' s ≃ s
where
toFun
x :=
⟨⟨f x, by simp⟩, by
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
simpa [apply_rangeSplitting f] using m⟩
invFun x := ⟨rangeSplitting f x, ⟨x, ⟨x.2, rfl⟩⟩⟩
left_inv
x := by
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
simp [apply_rangeSplitting f]
right_inv x := by simp [apply_rangeSplitting f]
