exists_lt_of_gauge_lt — Mathlib

English

If s is absorbent and gauge(s,x) < a, then there exists b with 0 < b < a and x ∈ b s.

Русский

Если s абсорбировано и gauge(s,x) < a, то существует b>0 и b<a такое, что x ∈ b s.

LaTeX

$$$$\\text{If } \\text{Absorbent}(\\mathbb{R}, s) \\text{ and } \\operatorname{gauge}(s,x) < a, \\text{ then } \\exists b>0:\\; b

Lean4

theorem exists_lt_of_gauge_lt (absorbs : Absorbent ℝ s) (h : gauge s x < a) : ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s :=
  by
  obtain ⟨b, ⟨hb, hx⟩, hba⟩ := exists_lt_of_csInf_lt absorbs.gauge_set_nonempty h
  exact ⟨b, hb, hba, hx⟩

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