to_countable

Mathlib.Data.Countable.Defs

URI: https://scilib.ai/kg/mathlib#Subsingleton.to_countable

English

Every subsingleton type is countable.

Русский

Любой тип с единственным элементом счётен.

LaTeX

$$$\text{Countable}(\alpha)\quad\text{for }\text{Subsingleton}(\alpha)$$$

Lean4

instance (priority := 100) to_countable [Subsingleton α] : Countable α :=
  ⟨⟨fun _ => 0, fun x y _ => Subsingleton.elim x y⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru