gauge_lt_one_eq_self_of_isOpen — Mathlib

English

If s is convex, 0 ∈ s and open, then gauge s x < 1 iff x ∈ s.

Русский

Если s выпукло, 0 ∈ s и открыто, то gauge s x < 1 тогда и только тогда x ∈ s.

LaTeX

$$$$(\\operatorname{Convex}_{\\mathbb{R}}(s)) \\land (0 \\in s) \\land (\\text{IsOpen } s) \\Rightarrow \\{x : \\mathrm{gauge}(s,x) < 1\\} = s.$$$$

Lean4

theorem gauge_lt_one_eq_self_of_isOpen (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : IsOpen s) :
    {x | gauge s x < 1} = s :=
  by
  refine (gauge_lt_one_subset_self hs₁ ‹_› <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀).antisymm ?_
  convert interior_subset_gauge_lt_one s
  exact hs₂.interior_eq.symm

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