fintype

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Subtype.fintype

English

For any predicate p, the subtype {x | p x} is a finite type, provided p is decidable and α is finite.

Русский

Для любого предиката p, при условии разрешимости и конечности α, подтип {x | p x} конечен.

LaTeX

$$$Fintype\{ x \;|\; p x \}$$$

Lean4

instance fintype (p : α → Prop) [DecidablePred p] [Fintype α] : Fintype { x // p x } :=
  Fintype.subtype (univ.filter p) (by simp)

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

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

Разделы

Аффилиация

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