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⟩