coe_abs — Mathlib

English

For any bounded continuous function f with values in a normed group that supports an absolute value, the absolute value of f, as a function, coincides with taking the pointwise absolute value of f: the map |f| is the function x ↦ |f(x)|.

Русский

Для любой ограниченно непрерывной функции f со значениями в группе с нормой и определенным модулем, абсолютное значение f как функция совпадает с поточечно взятым модулем: |f|(x) = |f(x)|.

LaTeX

$$$\forall f:\, \alpha \to^b \beta,\; (|f|)\,\wedge\,\text{as a function} = x \mapsto |f(x)|.$$$

Lean4

@[simp, norm_cast]
theorem coe_abs (f : α →ᵇ β) : ⇑|f| = |⇑f| :=
  rfl

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