continuous_norm' — Mathlib

English

The norm in NNReal is continuous under the topology, and so is the composition with the nonnegative norm map.

Русский

Норма в NNReal непрерывна, а также композиция с отображением ненегативной нормы непрерывна.

LaTeX

$$$ \text{continuous}_{{NNReal}}(\|\cdot\|) \quad \text{and} \quad \text{continuous}(.\,\text{nnnorm}). $$$

Lean4

@[to_additive (attr := continuity, fun_prop) continuous_norm]
theorem continuous_norm' : Continuous fun a : E => ‖a‖ := by
  simpa using continuous_id.dist (continuous_const : Continuous fun _a => (1 : E))

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