English
If s is convex, contains 0, and absorbs, and gauge s x = 1, then x lies on the boundary of s.
Русский
Если s выпукло, содержит 0 и абсорбирует, и gauge s x = 1, то x лежит на границе s.
LaTeX
$$$$ gauge\\, s\\, x = 1 \\Rightarrow x \\in \\partial s $$ \\\\ \\text{(under } s\\text{ convex},\\ 0\\in s,\\ Absorbent\\ s).$$$$
Lean4
theorem mem_frontier_of_gauge_eq_one (hc : Convex ℝ s) (hs₀ : 0 ∈ s) (ha : Absorbent ℝ s) (h : gauge s x = 1) :
x ∈ frontier s :=
⟨mem_closure_of_gauge_le_one hc hs₀ ha h.le, fun h' ↦ (interior_subset_gauge_lt_one s h').out.ne h⟩