English
For a family γ: α → Type, with all γ a denumerable type, the nth element of the dependent sum Σ γ has components given by the nth elements of α and γ.
Русский
Для семейства γ: α → Type, где каждая γ(a) денумерируема, n-й элемент зависимого суммирования Σ γ имеет компоненты: участок из α и соответствующее γ.
LaTeX
$$$ \text{ofNat}(\Sigma γ)\ n = \langle \text{ofNat } α (\mathrm{unpair}(n)).1, \text{ofNat}(\gamma (\text{ofNat } α (\mathrm{unpair}(n)).1)) (\mathrm{unpair}(n)).2 \rangle $$$
Lean4
@[simp]
theorem sigma_ofNat_val (n : ℕ) : ofNat (Sigma γ) n = ⟨ofNat α (unpair n).1, ofNat (γ _) (unpair n).2⟩ :=
Option.some.inj <| by rw [← decode_eq_ofNat, decode_sigma_val]; simp
