univ_shatters

Mathlib.Combinatorics.SetFamily.Shatter

URI: https://scilib.ai/kg/mathlib#Finset.univ_shatters

English

If α is finite, then the full family univ shatters every fixed s.

Русский

Пусть α конечно; тогда полное семейство подмножеств univ шаттерит любое фиксированное s.

LaTeX

$$$[Fintype\\, \\alpha] \\\\ univ.Shatters s$$$

Lean4

theorem univ_shatters [Fintype α] : univ.Shatters s :=
  shatters_of_forall_subset fun _ _ ↦ mem_univ _

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

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

Разделы

Аффилиация

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