gauge_gaugeRescale' — Mathlib

English

If gauge t x ≠ 0, then the gauge with respect to t of the rescaled point equals the gauge with respect to s of x: gauge t (gaugeRescale s t x) = gauge s x.

Русский

Если gauge t x ≠ 0, то gauge_t(gaugeRescale_s_t(x)) = gauge_s(x).

LaTeX

$$$\\operatorname{gauge}_t\\big(\\operatorname{gaugeRescale}(s,t,x)\\big) = \\operatorname{gauge}_s(x) \\quad\\text{assuming } \\operatorname{gauge}(t,x) \\neq 0$$$

Lean4

theorem gauge_gaugeRescale' (s : Set E) {t : Set E} {x : E} (hx : gauge t x ≠ 0) :
    gauge t (gaugeRescale s t x) = gauge s x := by
  rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)), smul_eq_mul,
    div_mul_cancel₀ _ hx]

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