gauge_lt_one_iff_mem_interior — Mathlib

English

The set {x | gauge s x < 1} equals interior s when s is convex and contains a neighborhood of 0.

Русский

Множество {x | gauge s x < 1} совпадает с interior s при выпуклости s и наличии окрестности 0.

LaTeX

$$$gauge s x < 1 \\iff x \\in interior s$$$

Lean4

theorem gauge_lt_one_iff_mem_interior (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) : gauge s x < 1 ↔ x ∈ interior s :=
  Set.ext_iff.1 (gauge_lt_one_eq_interior hc hs₀) _

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