one_le_gauge_of_notMem — Mathlib

English

If s is a star-convex at 0 and s absorbs a singleton {x}, and x ∉ s, then 1 ≤ gauge s x.

Русский

Если s звездо-выпукло относительно 0 и поглощает одноместный набор {x}, и x ∉ s, тогда 1 ≤ gauge s x.

LaTeX

$$$$(\\text{StarConvex}(0,s)) \\land (\\text{Absorbs}(s,{x})) \\land (x \\notin s) \\Rightarrow 1 \\le gauge(s,x).$$$$

Lean4

theorem one_le_gauge_of_notMem (hs₁ : StarConvex ℝ 0 s) (hs₂ : Absorbs ℝ s { x }) (hx : x ∉ s) : 1 ≤ gauge s x :=
  le_gauge_of_notMem hs₁ hs₂ <| by rwa [one_smul]

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