coe_const — Mathlib

English

The underlying function of the constant CauSeq at x is the constant function with value x: (const abv x) = Function.const ℕ x.

Русский

Базовая функция константной CauSeq на x равна константной функции значением x: (const abv x) = Function.const ℕ x.

LaTeX

$$$(\\text{CauSeq.const abv x}) = \\text{Function.const }\\mathbb{N} x$$$

Lean4

@[simp, norm_cast]
theorem coe_const (x : β) : (const x : ℕ → β) = Function.const ℕ x :=
  rfl

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