subset

Mathlib.Order.Partition.Finpartition

URI: https://scilib.ai/kg/mathlib#Finpartition.subset

English

Let P be a Finpartition of s. Then every block a ∈ P.parts satisfies a ⊆ s.

Русский

Пусть P—разбиение Finpartition s. Тогда любая часть a ∈ P.parts содержится в s.

LaTeX

$$$ a \in P.parts \Rightarrow a \subseteq s $$$

Lean4

theorem subset {a : Finset α} (ha : a ∈ P.parts) : a ⊆ s :=
  P.le ha

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

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

Разделы

Аффилиация

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