English
Let f be a function. The map S ↦ f[S] on subsets is injective iff f itself is injective.
Русский
Пусть f: α → β. Отображение подмножеств S ⊆ α в их образы f[S] инъективно тогда и только тогда, когда сам f инъективен.
LaTeX
$$$\operatorname{Injective}(\operatorname{image} f) \iff \operatorname{Injective} f$$$
Lean4
@[simp]
theorem image_injective : Injective (image f) ↔ Injective f :=
by
refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩
rw [← singleton_eq_singleton_iff]; apply h
rw [image_singleton, image_singleton, hx]