part_eq_of_mem — Mathlib

English

There exists an enumeration f : s ≃ Σ t ∈ P.parts, Fin #t.1 such that for all a,b ∈ s, P.part a = P.part b iff (f a).1 = (f b).1.

Русский

Существует отображение-биекция f : s ≃ Σ t ∈ P.parts, Fin #t.1, такое что для всех a,b ∈ s выполняется P.part a = P.part b ⇔ (f a).1 = (f b).1.

LaTeX

$$$ \exists f : s \simeq \sum_{t \in P.parts} \#t.1,\ \forall a,b \in s:\ P.part a = P.part b \iff (f a).1 = (f b).1 $$$

Lean4

theorem part_eq_of_mem (ht : t ∈ P.parts) (hat : a ∈ t) : P.part a = t :=
  (P.part_eq_iff_mem ht).2 hat

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