English
If f is injective on s, then s ≃ f''s via the natural forward map p ↦ f p and inverse given by a preimage choice.
Русский
Если функция f инъективна на s, то существует биекция s ≃ f''s, заданная естественным отображением p ↦ f p и обратным отображением по выбору предобраза.
LaTeX
$$Equiv s.Elem (Set.image f s).Elem$$
Lean4
/-- If a function `f` is injective on a set `s`, then `s` is equivalent to `f '' s`. -/
protected noncomputable def imageOfInjOn {α β} (f : α → β) (s : Set α) (H : InjOn f s) : s ≃ f '' s :=
⟨fun p => ⟨f p, mem_image_of_mem f p.2⟩, fun p => ⟨Classical.choose p.2, (Classical.choose_spec p.2).1⟩, fun ⟨_, h⟩ =>
Subtype.eq (H (Classical.choose_spec (mem_image_of_mem f h)).1 h (Classical.choose_spec (mem_image_of_mem f h)).2),
fun ⟨_, h⟩ => Subtype.eq (Classical.choose_spec h).2⟩
