image_injective — Mathlib

English

If f is injective, then image f is injective as a map on Finsets: s ≠ t implies s.image f ≠ t.image f.

Русский

Если f инъективна, то образ через f является инъективной функцией от конечных множеств: s ≠ t ⇒ s.image f ≠ t.image f.

LaTeX

$$$\text{Injective } f \Rightarrow \text{Injective } (\mathrm{image}\ f)$$$

Lean4

theorem image_injective (hf : Injective f) : Injective (image f) := by
  simpa only [funext (map_eq_image _)] using map_injective ⟨f, hf⟩

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