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' _ _