mem_openSegment_of_gauge_lt_one — Mathlib

English

If gauge s x < 1, then there exists y ∈ s such that x lies in the open segment from 0 to y.

Русский

Если gauge s x < 1, то существует y ∈ s такое, что x лежит на открытом отрезке [0,y].

LaTeX

$$$${\\exists\, y \\in E : y \\in s \\land x \\in \\operatorname{openSegment}_{\\mathbb{R}}(0,y)}.$$$$

Lean4

theorem mem_openSegment_of_gauge_lt_one (absorbs : Absorbent ℝ s) (hgauge : gauge s x < 1) :
    ∃ y ∈ s, x ∈ openSegment ℝ 0 y :=
  by
  rcases exists_lt_of_gauge_lt absorbs hgauge with ⟨r, hr₀, hr₁, y, hy, rfl⟩
  refine ⟨y, hy, 1 - r, r, ?_⟩
  simp [*]

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