English
There is a natural equivalence between the disjoint union ∐_{i∈Fin c.length} Fin (c.partSize i) and Fin n, given by (i,r) ↦ c.emb i r with inverse j ↦ (c.index j, c.invEmbedding j).
Русский
Существует естественное биективное соответствие между дизъюнктным объединением ∐_{i∈Fin c.length} Fin (c.partSize i) и Fin n, заданное отображениями (i,r) ↦ c.emb i r и обратным отображением j ↦ (c.index j, c.invEmbedding j).
LaTeX
$$$\\text{equivSigma} : ((i: \\mathrm{Fin} c.length) \\times \\mathrm{Fin}(c.partSize i)) \\simeq \\mathrm{Fin} n$$$
Lean4
/-- An ordered finpartition gives an equivalence between `Fin n` and the disjoint union of the
parts, each of them parameterized by `Fin (c.partSize i)`. -/
noncomputable def equivSigma : ((i : Fin c.length) × Fin (c.partSize i)) ≃ Fin n
where
toFun p := c.emb p.1 p.2
invFun i := ⟨c.index i, c.invEmbedding i⟩
right_inv _ := by simp
left_inv _ := by apply c.emb_injective; simp
