gauge_norm_smul — Mathlib

English

If s is balanced and 𝕜 is a normed field, then gauge s (‖r‖ • x) = gauge s (r • x).

Русский

Если s сбалансировано и 𝕜 — нормированное поле, то gauge s (‖r‖ • x) = gauge s (r • x).

LaTeX

$$$$\\mathrm{gauge}(s, \\|r\\| \\cdot x) = \\mathrm{gauge}(s, r \\cdot x).$$$$

Lean4

theorem gauge_norm_smul (hs : Balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (‖r‖ • x) = gauge s (r • x) :=
  by
  unfold gauge
  congr with θ
  rw [@RCLike.real_smul_eq_coe_smul 𝕜]
  refine and_congr_right fun hθ => (hs.smul _).smul_mem_iff ?_
  rw [RCLike.norm_ofReal, abs_norm]

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