mem_part_self

Mathlib.Order.Partition.Finpartition

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

← MathLib Explorer

English

For any a, a ∈ P.part a if and only if a ∈ s.

Русский

Для каждого a выполняется: a входит в P.part a тогда и только тогда, когда a ∈ s.

LaTeX

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

Lean4

@[simp]
theorem mem_part_self : a ∈ P.part a ↔ a ∈ s := by
  by_cases ha : a ∈ s
  · simp [part, ha, choose_property (p := fun s => a ∈ s) P.parts (P.existsUnique_mem ha)]
  · simp [P.part_eq_empty.2, ha]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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