slice_subset

Mathlib.Data.Finset.Slice

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

English

Every r-th slice is a subset of 𝒜.

Русский

Каждый r-й срез является подмножеством 𝒜.

LaTeX

$$$ 𝒜_{r} \subseteq 𝒜 $$$

Lean4

/-- The `r`-th slice of `𝒜` is a subset of `𝒜`. -/
theorem slice_subset : 𝒜 #r ⊆ 𝒜 :=
  filter_subset _ _

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

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

Разделы

Аффилиация

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