gauge_lt_one_subset_self — Mathlib

English

If s is convex, 0 ∈ s, and s is absorbent, then {x : gauge s x < 1} ⊆ s.

Русский

Пусть s выпукло, 0 ∈ s и s поглощающее. Тогда {x : gauge s x < 1} ⊆ s.

LaTeX

$$$$(\\operatorname{Convex}_{\\mathbb{R}}(s)) \\land (0 \\in s) \\land (\\operatorname{Absorbent}_{\\mathbb{R}}(s)) \\Rightarrow \\{x \\in E \\mid \\mathrm{gauge}(s,x) < 1\\} \\subseteq s.$$$$

Lean4

theorem gauge_lt_one_subset_self (hs : Convex ℝ s) (h₀ : (0 : E) ∈ s) (absorbs : Absorbent ℝ s) :
    {x | gauge s x < 1} ⊆ s := fun _x hx ↦
  let ⟨_y, hys, hx⟩ := mem_openSegment_of_gauge_lt_one absorbs hx
  hs.openSegment_subset h₀ hys hx

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