isEmpty'

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#Fin.isEmpty'

English

The type Fin Nat.zero is empty (equivalent to Fin 0).

Русский

Тип Fin Nat.zero пуст (эквивалентен Fin 0).

LaTeX

$$$ \mathrm{IsEmpty}(\mathrm{Fin}(\mathrm{Nat}.zero)) $$$

Lean4

instance isEmpty' : IsEmpty (Fin Nat.zero) :=
  Fin.isEmpty

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

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

Разделы

Аффилиация

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