image_nontrivial_iff — Mathlib

English

For an injective map, (f''s).Subsingleton is equivalent to s.Subsingleton.

Русский

Для инъективного отображения (f''s).Subsingleton эквивалентно s.Subsingleton.

LaTeX

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

Lean4

@[simp]
theorem image_nontrivial_iff (hf : s.InjOn f) : (f '' s).Nontrivial ↔ s.Nontrivial :=
  ⟨nontrivial_of_image f s, fun h ↦ h.image_of_injOn hf⟩

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