mabs_apply — Mathlib

English

As above, the pointwise absolute value of a continuous map equals the absolute value of its values at each point.

Русский

То же самое: точечное абсолютное значение непрерывного отображения равно абсолютному значению его значений в каждой точке.

LaTeX

$$$\\forall f:\\, C(\\alpha, \\beta),\\; \\forall x:\\, \\alpha:\\; |f|_m\\,x = |f(x)|_m$$$

Lean4

@[to_additive (attr := simp)]
theorem mabs_apply (f : C(α, β)) (x : α) : |f|ₘ x = |f x|ₘ :=
  rfl

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