gauge_eq_one_iff_mem_frontier — Mathlib

English

Under convex, nhds(0)-neighborhood, gauge s x = 1 is equivalent to x lying on the frontier of s.

Русский

При выпуклости, gauge s x = 1 эквивалентно тому, что x лежит на границе s.

LaTeX

$$$$ gauge s x = 1 \\iff x \\in \\partial s, \\quad (s \\text{ convex},\\ 0 \\in nhds(0)). $$$$

Lean4

theorem gauge_eq_one_iff_mem_frontier (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) : gauge s x = 1 ↔ x ∈ frontier s :=
  by
  rw [eq_iff_le_not_lt, gauge_le_one_iff_mem_closure hc hs₀, gauge_lt_one_iff_mem_interior hc hs₀]
  rfl

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