part_mem

Mathlib.Order.Partition.Finpartition

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

English

P.part a ∈ P.parts if and only if a ∈ s.

Русский

Членство P.part a в P.parts эквивалентно a ∈ s.

LaTeX

$$$ P.part a \in P.parts \iff a \in s $$$

Lean4

@[simp]
theorem part_mem : P.part a ∈ P.parts ↔ a ∈ s := by by_cases ha : a ∈ s <;> simp [part, ha, choose_mem]

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

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

Разделы

Аффилиация

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