enorm — Mathlib

English

If f is continuous within a set s at a point a, then the EN-norm of f is continuous within s at a.

Русский

Если f непрерывна внутри множества s в точке a, то ‖f·‖ₑ непрерывна внутри s в a.

LaTeX

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

Lean4

@[fun_prop]
theorem enorm {s : Set X} {a : X} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (‖f ·‖ₑ) s a :=
  (ContinuousENorm.continuous_enorm.continuousWithinAt).comp (t := Set.univ) h (fun _ _ ↦ by trivial)

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