norm_expMapBasis_ne_zero — Mathlib

English

The log mapped image of expMapBasis is nonnegative coordinatewise in the fundamental cone.

Русский

Логарифмированное изображение expMapBasis неотрицательно по каждой координате внутри фундаментальной конусы.

LaTeX

$$$\forall x, \ logMap(\text{mixedSpaceOfRealSpace}(\text{expMapBasis}(x))) \in ZSpan.fundamentalDomain(\cdot) \Rightarrow x_w \ge 0$$$

Lean4

theorem norm_expMapBasis_ne_zero (x : realSpace K) : mixedEmbedding.norm (mixedSpaceOfRealSpace (expMapBasis x)) ≠ 0 :=
  norm_expMapBasis x ▸ pow_ne_zero _ (Real.exp_ne_zero _)

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