English
For a family of types σ(a) indexed by a in α, and a list l1 of α, the length of the sigma-list l1.sigma l2 equals the sum over a in l1 of the length of l2(a): length(l1.sigma l2) = sum over a of length(l2(a)).
Русский
Для семейства типов σ(a) индексированного по a∈α и списка l1 из α длина списка-сига l1.sigma l2 равна сумме длин волокон: длина(l1.sigma l2) = сумма по a∈l1 длины(l2(a)).
LaTeX
$$$\text{length}(\,l_1.\text{sigma}\, l_2) = \bigl(\sum_{a \in l_1} \text{length}(l_2(a))\bigr)$$$
Lean4
theorem length_sigma {σ : α → Type*} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
length (l₁.sigma l₂) = (l₁.map fun a ↦ length (l₂ a)).sum := by
induction l₁ with
| nil => rfl
| cons x l₁ IH => simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]
