subsingleton — Mathlib

English

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

Русский

Если функция f: α → β инъективна, а β субодиночен, то α субодиночен.

LaTeX

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

Lean4

/-- If the codomain of an injective function is a subsingleton, then the domain
is a subsingleton as well. -/
protected theorem subsingleton (hf : Injective f) [Subsingleton β] : Subsingleton α :=
  ⟨fun _ _ ↦ hf <| Subsingleton.elim _ _⟩

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