subsingleton — Mathlib

English

If α is subsingleton and f: α → β is surjective, then β is subsingleton.

Русский

Если область α субодиночна и f: α → β сюръективна, то β субодиночен.

LaTeX

$$$\\\\operatorname{Subsingleton}(\\\\beta) \\\\text{ given } [\\\\operatorname{Subsingleton}(\\\\alpha)] \\\\text{ and } \\\\operatorname{Surjective}(f).$$$

Lean4

/-- If the domain of a surjective function is a subsingleton, then the codomain is a subsingleton as
well. -/
protected theorem subsingleton [Subsingleton α] (hf : Surjective f) : Subsingleton β :=
  ⟨hf.forall₂.2 fun x y ↦ congr_arg f <| Subsingleton.elim x y⟩

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