gauge_def' — Mathlib

English

Another equivalent expression for gauge uses the inverse scalar acting on x.

Русский

Еще одно эквивалентное выражение gauge через обратное действие скаляра на x.

LaTeX

$$$$\\operatorname{gauge}(s,x) = \\inf\\{ r>0 : r^{-1} x \\in s \\}.$$$$

Lean4

/-- An alternative definition of the gauge using scalar multiplication on the element rather than on
the set. -/
theorem gauge_def' : gauge s x = sInf ({r ∈ Set.Ioi (0 : ℝ) | r⁻¹ • x ∈ s}) :=
  by
  congrm sInf {r | ?_}
  exact and_congr_right fun hr => mem_smul_set_iff_inv_smul_mem₀ hr.ne' _ _

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