mem_frontier_of_gauge_eq_one — Mathlib

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⟩

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