image_of_injOn — Mathlib

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 ·)⟩

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