subsingleton_dom — Mathlib

English

If the domain α is a subsingleton, then any EquivLike-like structure E is also a subsingleton.

Русский

Если домен α состоит из одного элемента, то любая структура EquivLike-подобная тоже является Subsingleton.

LaTeX

$$$[Subsingleton\ α] \Rightarrow \text{Subsingleton}(E)$$$

Lean4

/-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search. -/
theorem subsingleton_dom [Subsingleton α] : Subsingleton E :=
  ⟨fun f g ↦ DFunLike.ext f g fun _ ↦ (right_inv f).injective <| Subsingleton.elim _ _⟩

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