image_injective — Mathlib

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]

Похожие утверждения