image — Mathlib

English

The image of a nontrivial set under an injective map is nontrivial.

Русский

Образ непустого множества под инъективной функцией не тривиален.

LaTeX

$$$s.Nontrivial \Rightarrow (f''s).Nontrivial$ (при $f$ инъективной).$$

Lean4

/-- The image of a nontrivial set under an injective map is nontrivial. -/
theorem image (hs : s.Nontrivial) (hf : Function.Injective f) : (f '' s).Nontrivial :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨f x, mem_image_of_mem f hx, f y, mem_image_of_mem f hy, hf.ne hxy⟩

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