Subsingleton — Mathlib

English

If the base type is Subsingleton, then the quotient by any relation is Subsingleton.

Русский

Если база является Subsingleton, то фактор-множество по любой отношении тоже Subsingleton.

LaTeX

$$$$\text{[Subsingleton } \alpha]\;\Rightarrow\; \text{Subsingleton } (Quot ra).$$$$

Lean4

protected instance Subsingleton [Subsingleton α] : Subsingleton (Quot ra) :=
  ⟨fun x ↦ Quot.induction_on x fun _ ↦ Quot.ind fun _ ↦ congr_arg _ (Subsingleton.elim _ _)⟩

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