fintypeTop

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.fintypeTop

English

The top set ⊤ has a finite type structure, inherited from univ.

Русский

Верхнее множество ⊤ имеет структуру конечного типа, наследуемую от univ.

LaTeX

$$$ \text{Fintype}(\top : \mathrm{Set}\alpha) $$$

Lean4

instance fintypeTop [Fintype α] : Fintype (⊤ : Set α) :=
  inferInstanceAs (Fintype (univ : Set α))

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

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

Разделы

Аффилиация

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