normAtAllPlaces_mixedSpaceOfRealSpace

English

If x is a real-space function with nonnegative values, then normAtAllPlaces on the real-space embedding equals x.

Русский

Если x — функция реального пространства с неотрицательными значениями, то нормa на всех местах для встраивания в реальное пространство совпадает с x.

LaTeX

$$$$\operatorname{normAtAllPlaces}(\operatorname{mixedSpaceOfRealSpace}(x)) = x \quad\text{given } x(w) \ge 0\,\forall w.$$$$

Lean4

theorem normAtAllPlaces_mixedSpaceOfRealSpace {x : realSpace K} (hx : ∀ w, 0 ≤ x w) :
    normAtAllPlaces (mixedSpaceOfRealSpace x) = x := by
  ext
  rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hx _)]

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