gaugeRescale_self_apply — Mathlib

English

For absorbent s and von Neumann bounded s, gaugeRescale s s x = x for all x.

Русский

При абсорбируемом s и ограниченности по фон Неймана выполняется gaugeRescale s s x = x для всех x.

LaTeX

$$$\\operatorname{gaugeRescale}(s,s,x) = x$$$

Lean4

theorem gaugeRescale_self_apply {s : Set E} (hsa : Absorbent ℝ s) (hsb : IsVonNBounded ℝ s) (x : E) :
    gaugeRescale s s x = x := by
  rcases eq_or_ne x 0 with rfl | hx; · simp
  rw [gaugeRescale, div_self, one_smul]
  exact ((gauge_pos hsa hsb).2 hx).ne'

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