stdBasis — Mathlib

English

The global norm equals zero exactly when some local norm is zero (variant).

Русский

Глобальная норма равна нулю тогда и только тогда, когда какая-то локальная норма равна нулю.

LaTeX

$$$ \|x\| = 0 \iff \exists w, \operatorname{normAtPlace}(w, x) = 0 $$$

Lean4

/-- The `ℝ`-basis of the mixed space of `K` formed by the vector equal to `1` at `w` and `0`
elsewhere for `IsReal w` and by the couple of vectors equal to `1` (resp. `I`) at `w` and `0`
elsewhere for `IsComplex w`. -/
def stdBasis : Basis (index K) ℝ (mixedSpace K) :=
  Basis.prod (Pi.basisFun ℝ _) (Basis.reindex (Pi.basis fun _ => basisOneI) (Equiv.sigmaEquivProd _ _))

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