fintypeMemFinset

Mathlib.Data.Set.Finite.Basic

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

English

For a Finset s, the set {a | a ∈ s} is finite.

Русский

Для конечного множества s множество {a | a ∈ s} конечно.

LaTeX

$$$\\operatorname{Finite}\\bigl(\\{a \\mid a \\in s\\}\\bigr).$$$

Lean4

instance fintypeMemFinset (s : Finset α) : Fintype {a | a ∈ s} :=
  Finset.fintypeCoeSort s

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

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

Разделы

Аффилиация

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