fintypePure

Mathlib.Data.Set.Finite.Monad

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

English

For any a, the singleton set {a} in Set α is finite.

Русский

Для любого элемента a множество-одиночка {a} в Set α конечно.

LaTeX

$$Fintype (pure a : Set α)$$

Lean4

instance fintypePure : ∀ a : α, Fintype (pure a : Set α) :=
  Set.fintypeSingleton

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

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

Разделы

Аффилиация

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