disjointedRec_zero — Mathlib

English

The zero-case of disjointedRec reduces to the base case: disjointedRec hdiff h0 equals disjointed_zero f applied to h0.

Русский

Базовый случай disjointedRec сводится к нулевому случаю: disjointedRec hdiff h0 равно disjointed_zero f, применённому к h0.

LaTeX

$$$ \mathrm{Nat.disjointedRec}\; hdiff\; h_0 = (\mathrm{disjointed_zero} f \;\; h_0) $$$

Lean4

@[simp]
theorem disjointedRec_zero {f : ℕ → α} {p : α → Sort*} (hdiff : ∀ ⦃t i⦄, p t → p (t \ f i)) (h₀ : p (f 0)) :
    Nat.disjointedRec hdiff h₀ = (disjointed_zero f ▸ h₀) :=
  rfl

Похожие утверждения