continuous_norm — Mathlib

English

The function x ↦ mixedEmbedding.norm(x) is continuous on the mixed space.

Русский

Функция x ↦ mixedEmbedding.norm(x) непрерывна на смешанном пространстве.

LaTeX

$$$ \text{Continuous}( \operatorname{mixedEmbedding.norm} ) $$$

Lean4

@[fun_prop]
protected theorem continuous_norm : Continuous (mixedEmbedding.norm : (mixedSpace K) → ℝ) :=
  by
  refine continuous_finset_prod Finset.univ fun _ _ ↦ ?_
  simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dite_pow]
  split_ifs <;> fun_prop

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