sized_slice

Mathlib.Data.Finset.Slice

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

English

All elements of the r-th slice have size r.

Русский

Все элементы r-го среза имеют размер r.

LaTeX

$$$ (𝒜 #r : Set (Finset α)).Sized r $$$

Lean4

/-- Everything in the `r`-th slice of `𝒜` has size `r`. -/
theorem sized_slice : (𝒜 #r : Set (Finset α)).Sized r := fun _ => And.right ∘ mem_slice.mp

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

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

Разделы

Аффилиация

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