gauge_lt_one_eq_interior — Mathlib

English

For a convex set s with nhds 0 containing s, gauge s x < 1 iff x ∈ interior s.

Русский

Для выпуклого s и nhds 0, если gauge s x < 1 тогда x внутри interior s, иначе наоборот.

LaTeX

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

Lean4

theorem gauge_lt_one_eq_interior (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) : {x | gauge s x < 1} = interior s :=
  by
  refine Subset.antisymm (fun x hx ↦ ?_) (interior_subset_gauge_lt_one s)
  rcases mem_openSegment_of_gauge_lt_one (absorbent_nhds_zero hs₀) hx with ⟨y, hys, hxy⟩
  exact hc.openSegment_interior_self_subset_interior (mem_interior_iff_mem_nhds.2 hs₀) hys hxy

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