instSubsingleton — Mathlib

English

For every F, the height-0 approximation CofixA F 0 has at most one element; it is a singleton type.

Русский

Для любого F высота-0 приближения CofixA F 0 является единичным типом (в нём не может быть двух разных элементов).

LaTeX

$$$\\operatorname{Subsingleton}\\big(\\operatorname{CofixA} F 0\\big)$$$

Lean4

instance instSubsingleton : Subsingleton (CofixA F 0) :=
  ⟨by rintro ⟨⟩ ⟨⟩; rfl⟩

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