enorm — Mathlib

English

If f is continuous on a set s around a point a (ContinuousWithinAt f s a), then the function x ↦ ‖f x‖ₑ is also continuous within the same set at a.

Русский

Если f непрерывна внутри множества s в окрестности точки a, то функция x ↦ ‖f x‖ₑ непрерывна внутри того же множества в точке a.

LaTeX

$$$\\text{ContinuousWithinAt}(f,s,a) \\Rightarrow \\text{ContinuousWithinAt}\\bigl(x \\mapsto \\|f(x)\\|_\\varepsilon\\bigr)\\; s\\ a$$$

Lean4

@[fun_prop]
theorem enorm : Continuous f → Continuous (‖f ·‖ₑ) :=
  continuous_enorm.comp

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