image_nontrivial — Mathlib

English

For an injective map, the image of a set is nontrivial if and only if the set is nontrivial.

Русский

Для инъективного отображения образ множества не тривиален тогда и только тогда, когда само множество не тривиально.

LaTeX

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

Lean4

@[simp]
theorem image_nontrivial (hf : f.Injective) : (f '' s).Nontrivial ↔ s.Nontrivial :=
  ⟨nontrivial_of_image f s, fun h ↦ h.image hf⟩

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