eq_of_mem_parts

Mathlib.Order.Partition.Finpartition

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

← MathLib Explorer

English

If t,u ∈ P.parts and a ∈ t ∩ u, then t = u.

Русский

Если t,u ∈ P.parts и a ∈ t ∩ u, то t = u.

LaTeX

$$$ t \in P.parts \land u \in P.parts \land a \in t \land a \in u \Rightarrow t = u $$$

Lean4

theorem eq_of_mem_parts (ht : t ∈ P.parts) (hu : u ∈ P.parts) (hat : a ∈ t) (hau : a ∈ u) : t = u :=
  P.disjoint.elim ht hu <| not_disjoint_iff.2 ⟨a, hat, hau⟩

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

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

Разделы

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

Аффилиация

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