gaugeRescale_def — Mathlib

English

The gauge rescale map gaugeRescale s t x is defined by the formula gauge s x divided by gauge t x, scaled along x.

Русский

Пере масштаб gauge задаётся формулой gauge s x / gauge t x, умножаемой на x.

LaTeX

$$$\\operatorname{gaugeRescale}(s,t,x) = \\left(\\dfrac{\\operatorname{gauge}(s,x)}{\\operatorname{gauge}(t,x)}\\right) \\cdot x$$$

Lean4

theorem gaugeRescale_def (s t : Set E) (x : E) : gaugeRescale s t x = (gauge s x / gauge t x) • x :=
  rfl

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