subsingleton_image_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem subsingleton_image_iff (hf : Injective f) {s : Set α} : (f '' s).Subsingleton ↔ s.Subsingleton :=
  ⟨subsingleton_of_image hf s, fun h => h.image f⟩

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