sized_falling

Mathlib.Combinatorics.SetFamily.LYM

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

English

The falling operator preserves the required size: the resulting sets have the prescribed cardinality.

Русский

Оператор падения сохраняет требуемый размер: полученные множества имеют заданную кардинальность.

LaTeX

$$$\mathrm{falling}\ k\ 𝒜 :\; \text{Sized } k$$$

Lean4

theorem sized_falling : (falling k 𝒜 : Set (Finset α)).Sized k := fun _ hs => (mem_falling.1 hs).2

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

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

Разделы

Аффилиация

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