equivSigmaParts — Mathlib

English

There is an equivalence between the subset s and the dependent sum over the parts: s ≃ Σ t ∈ P.parts, t.1.

Русский

Существует эквивалентность между множеством s и зависимой суммой по частям: s ≃ Σ t ∈ P.parts, t.1.

LaTeX

$$$ s \simeq \sum_{t \in P.parts} t.1 $$$

Lean4

/-- Equivalence between a finpartition's parts as a dependent sum and the partitioned set. -/
def equivSigmaParts : s ≃ Σ t : P.parts, t.1
    where
  toFun x := ⟨⟨P.part x.1, P.part_mem.2 x.2⟩, ⟨x, P.mem_part x.2⟩⟩
  invFun x := ⟨x.2, mem_of_subset (P.le x.1.2) x.2.2⟩
  left_inv x := by simp
  right_inv
    x := by
    ext e
    · obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x
      dsimp only at mf ⊢
      rw [P.part_eq_of_mem mp mf]
    · simp

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