subsingleton_of_image — Mathlib

English

If the image f''s is subsingleton, then s is a subsingleton provided f is injective.

Русский

Если образ f''s является подсинглтонным, то s также подсинглтонно, при условии, что f инъективно отображает s.

LaTeX

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

Lean4

/-- If the image of a set under an injective map is a subsingleton, the set is a subsingleton. -/
theorem subsingleton_of_image (hf : Function.Injective f) (s : Set α) (hs : (f '' s).Subsingleton) : s.Subsingleton :=
  (hs.preimage hf).anti <| subset_preimage_image _ _

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