English
There is a natural bijection between the disjoint sum of the blocks (as pairs (i, j) with i ∈ Fin c.length and j ∈ Fin (c.blocksFun i)) and Fin n, given by the embedding and its inverse.
Русский
Существует естественная биекция между объединением блоков (в виде пар (i, j) с i ∈ Fin c.length и j ∈ Fin (c.blocksFun i)) и Fin n, задаваемая вложением и его обратной связью.
LaTeX
$$$ blocksFinEquiv : (\\Sigma i : Fin c.length, Fin (c.blocksFun i)) \\simeq Fin n $$$
Lean4
/-- Equivalence between the disjoint union of the blocks (each of them seen as
`Fin (c.blocksFun i)`) with `Fin n`. -/
def blocksFinEquiv : (Σ i : Fin c.length, Fin (c.blocksFun i)) ≃ Fin n
where
toFun x := c.embedding x.1 x.2
invFun j := ⟨c.index j, c.invEmbedding j⟩
left_inv
x := by
rcases x with ⟨i, y⟩
dsimp
congr; · exact c.index_embedding _ _
rw [Fin.heq_ext_iff]
· exact c.invEmbedding_comp _ _
· rw [c.index_embedding]
right_inv j := c.embedding_comp_inv j
