logMap_real_smul — Mathlib

English

Let x be a nonzero element in the mixed space and c a nonzero real number. Then the logarithmic embedding is constant along the real ray through x: logMap(c · x) = logMap(x).

Русский

Пусть x лежит в перемешанном пространстве и c — не нуль-число. Тогда логарифмическое отображение сохраняется при масштабировании: logMap(c · x) = logMap(x).

LaTeX

$$$\forall x\in \text{mixedSpace }K,\; \forall c\in \mathbb{R},\; c\neq 0 \Rightarrow\ logMap(c\cdot x) = logMap(x),$ при условии $\,\,\, \; \text{norm}(x) \neq 0$.$$

Lean4

theorem logMap_real_smul (hx : mixedEmbedding.norm x ≠ 0) {c : ℝ} (hc : c ≠ 0) : logMap (c • x) = logMap x :=
  by
  have : mixedEmbedding.norm (c • (1 : mixedSpace K)) ≠ 0 :=
    by
    rw [norm_smul, map_one, mul_one]
    exact pow_ne_zero _ (abs_ne_zero.mpr hc)
  rw [← smul_one_mul, logMap_mul this hx, logMap_real, zero_add]

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