normAtAllPlaces_normAtAllPlaces — Mathlib

English

Norms computed via different representations (mixedSpaceOfRealSpace) agree with the global norm At All Places.

Русский

Нормы, получаемые через разные представления, согласованы с глобальной нормой на всех местах.

LaTeX

$$$$\operatorname{normAtAllPlaces}(\operatorname{mixedSpaceOfRealSpace}(\operatorname{normAtAllPlaces}(x))) = \operatorname{normAtAllPlaces}(x).$$$$

Lean4

theorem normAtAllPlaces_normAtAllPlaces (x : mixedSpace K) :
    normAtAllPlaces (mixedSpaceOfRealSpace (normAtAllPlaces x)) = normAtAllPlaces x :=
  normAtAllPlaces_mixedSpaceOfRealSpace fun _ ↦ (normAtAllPlaces_nonneg _ _)

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