exists_enumeration — Mathlib

English

There exists a bijection f : s ≃ Σ t : P.parts, Fin #t.1 such that for all a,b : s, P.part a = P.part b ↔ (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 exists_enumeration : ∃ f : s ≃ Σ t : P.parts, Fin #t.1, ∀ a b : s, P.part a = P.part b ↔ (f a).1 = (f b).1 :=
  by
  use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))
  simp [equivSigmaParts, Equiv.sigmaCongr, Equiv.sigmaCongrLeft]

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