continuous_nnnorm' — Mathlib

English

The norm map and its nn-norm version are continuous; for any f: α → E, if f is continuous then ‖f‖ and ‖f‖₊ are continuous as functions α → R≥0.

Русский

Отображения ‖f‖ и ‖f‖₊ непрерывны, если f: α → E непрерывна.

LaTeX

$$$ \text{continuous}_{{f}}(\|f\|) \quad \text{and} \quad \text{continuous}_{{f}}(\|f\|_+). $$$

Lean4

@[to_additive (attr := continuity, fun_prop) continuous_nnnorm]
theorem continuous_nnnorm' : Continuous fun a : E => ‖a‖₊ :=
  continuous_norm'.subtype_mk _

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