norm_eq_sup'_normAtPlace — Mathlib

English

The global norm equals the supremum over nonempty index set of local norms, i.e., norm equals the sup over w of normAtPlace w x.

Русский

Глобальная норма равна супремуму по всем непустым индексам локальных норм: норма равна sup_w normAtPlace(w, x).

LaTeX

$$$ \|x\| = \sup^{'}_{w \in \mathrm{InfinitePlace}(K)} \operatorname{normAtPlace}(w, x) $$$

Lean4

theorem norm_eq_sup'_normAtPlace (x : mixedSpace K) : ‖x‖ = univ.sup' univ_nonempty fun w ↦ normAtPlace w x :=
  by
  rw [← coe_nnnorm, nnnorm_eq_sup_normAtPlace, ← sup'_eq_sup univ_nonempty, ← NNReal.val_eq_coe, ←
    OrderHom.Subtype.val_coe, map_finset_sup', OrderHom.Subtype.val_coe]
  simp only [Function.comp_apply]

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