subsingleton_of_preimage — Mathlib

English

If a preimage of a set under a surjective map is a subsingleton, then the set is a subsingleton.

Русский

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

LaTeX

$$$(f^{-1} s).Subsingleton \Rightarrow s.Subsingleton$ при $f$ сюръективной.$$

Lean4

/-- If the preimage of a set under a surjective map is a subsingleton,
the set is a subsingleton. -/
theorem subsingleton_of_preimage (hf : Function.Surjective f) (s : Set β) (hs : (f ⁻¹' s).Subsingleton) :
    s.Subsingleton := fun fx hx fy hy =>
  by
  rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
  exact congr_arg f (hs hx hy)

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