infty_coeFn_natCast — Mathlib

English

The natural-number casting into the ∞-normed product acts as the identity on the underlying function, i.e., the coeFn of the nat-cast is the same as the constant function.

Русский

Приведение по натуральному числу в произведение с нормой ∞ действует как идентичность на базовой функции; координатная функция совпадает с константой.

LaTeX

$$$\bigl( n \bigr)^{\wedge} = n \quad\text{as functions, i.e. } ~(n : \lp B\!\infty)_i = n.$$$

Lean4

@[simp]
theorem infty_coeFn_natCast (n : ℕ) : ⇑(n : lp B ∞) = n :=
  rfl

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