recTopCoe_ofNat — Mathlib

English

For all C, d ∈ C ⊤, f : ∀ a ∈ ℕ, C a, x ∈ ℕ with x ≥ 2, recTopCoe d f ofNat(x) = f(ofNat(x)).

Русский

Для любого C, d ∈ C ⊤, f : ∀ a ∈ ℕ, C a, и x ∈ ℕ, такого что x ≥ 2, recTopCoe d f ofNat(x) = f(ofNat(x)).

LaTeX

$$$\\\\forall {C : ENat \\\\to \\\\text{Sort}*} (d : C \\\\top) (f : \\\\forall a : \\\\mathbb{N}, C a), (x : \\\\mathbb{N}) \\\\Big[ x.AtLeastTwo \\\\Big] \\\\Rightarrow @\\\\recTopCoe C d f (\\\\operatorname{ofNat}(x)) = f(\\\\operatorname{OfNat}(x)).$$$

Lean4

@[simp]
theorem recTopCoe_ofNat {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) [x.AtLeastTwo] :
    @recTopCoe C d f ofNat(x) = f (OfNat.ofNat x) :=
  rfl

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