instCoeFunForallNat — Mathlib

English

There is a canonical CoeFun from CauSeq β abv to ℕ → β given by the first projection.

Русский

Существует каноническое отображение-коэрсион из CauSeq β abv в ℕ → β, задаваемое проекцией на первое слагаемое.

LaTeX

$$$\\text{coe}: \\CauSeq(\\beta,abv) \\to (\\mathbb{N} \\to \\beta),\\quad f \\mapsto f$$$

Lean4

instance : CoeFun (CauSeq β abv) fun _ => ℕ → β :=
  ⟨Subtype.val⟩

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