setFintype

Mathlib.Data.Fintype.Sets

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

← MathLib Explorer

English

If α is finite, then for any set s ⊆ α, the subtype s is finite: Fintype s.Elem.

Русский

Если α конечно, то для каждого множества s ⊆ α подтип s конечен: Fintype s.Elem.

LaTeX

$$$Fintype( s.Elem )$$$

Lean4

/-- A set on a fintype, when coerced to a type, is a fintype. -/
def setFintype [Fintype α] (s : Set α) [DecidablePred (· ∈ s)] : Fintype s :=
  Subtype.fintype fun x => x ∈ s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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