continuous_enorm — Mathlib

English

Let E be a space with EN-norm. The map a ↦ ‖a‖ₑ is continuous on its domain; i.e., the EN-norm is a continuous function.

Русский

Пусть у E задана EN-норма. Оценка ‖a‖ₑ является непрерывной функцией на области определения.

LaTeX

$$$\\text{ContinuousENorm}$ implies $\\|\\cdot\\|_\\varepsilon$ is a continuous function on E; more precisely, $\\forall a, \\; \\text{Continuous}(a \\mapsto \\|a\\|_\\varepsilon)$.$$

Lean4

@[continuity, fun_prop]
theorem continuous_enorm : Continuous fun a : E ↦ ‖a‖ₑ :=
  ContinuousENorm.continuous_enorm

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