English
There is a canonical equivalence between the dependent sum over ℕ of f(n) and the coproduct f(0) ⊕ Σn f(n+1).
Русский
Существует каноническое эквивалентность между суммой по зависимостям над ℕ: Σn f(n) и разложение f(0) ⊕ Σn f(n+1).
LaTeX
$$$$ (\\Sigma n, f(n)) \\simeq f(0) \\oplus \\Sigma n, f(n+1). $$$$
Lean4
/-- An equivalence that separates out the 0th fiber of `(Σ (n : ℕ), f n)`. -/
def sigmaNatSucc (f : ℕ → Type u) : (Σ n, f n) ≃ f 0 ⊕ Σ n, f (n + 1) :=
⟨fun x =>
@Sigma.casesOn ℕ f (fun _ => f 0 ⊕ Σ n, f (n + 1)) x fun n =>
@Nat.casesOn (fun i => f i → f 0 ⊕ Σ n : ℕ, f (n + 1)) n (fun x : f 0 => Sum.inl x) fun (n : ℕ) (x : f n.succ) =>
Sum.inr ⟨n, x⟩,
Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun _ => id), by rintro ⟨n | n, x⟩ <;> rfl, by
rintro (x | ⟨n, x⟩) <;> rfl⟩
