finZeroEquiv

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#finZeroEquiv

English

There is a canonical equivalence between Fin 0 and the empty type.

Русский

Существует каноническая эквивалентность между Fin 0 и пустым типом.

LaTeX

$$$ \text{finZeroEquiv}: Fin 0 \simeq Empty $$$

Lean4

/-- Equivalence between `Fin 0` and `Empty`. -/
def finZeroEquiv : Fin 0 ≃ Empty :=
  .equivEmpty _

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

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

Разделы

Аффилиация

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