English
If a set is nontrivial and f is injective on that set, then its image is nontrivial.
Русский
Если множество не тривиально и отображение инъективно на этом множестве, то его образ не тривиален.
LaTeX
$$$s.Nontrivial \Rightarrow (f''s).Nontrivial$ при $s$-множество, на котором $f$ инъективно.$$
Lean4
theorem image_of_injOn (hs : s.Nontrivial) (hf : s.InjOn f) : (f '' s).Nontrivial :=
by
obtain ⟨x, hx, y, hy, hxy⟩ := hs
exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩