part_eq_iff_mem

Mathlib.Order.Partition.Finpartition

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

← MathLib Explorer

English

If t ∈ P.parts, then P.part a = t ↔ a ∈ t.

Русский

Если t ∈ P.parts, то P.part a = t ⇔ a ∈ t.

LaTeX

$$$ P.part a = t \iff a \in t \quad (t \in P.parts) $$$

Lean4

theorem part_eq_iff_mem (ht : t ∈ P.parts) : P.part a = t ↔ a ∈ t :=
  by
  constructor
  · rintro rfl
    simp_all
  · intro hat
    apply P.eq_of_mem_parts (a := a) <;> simp [*, P.le ht hat]

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

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

Разделы

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

Аффилиация

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