exists_between_self_add — Mathlib

English

If s has a greatest lower bound a, then for any ε>0 there exists b in s with a ≤ b < a+ε.

Русский

Если s имеет наибольшую нижнюю грань a, то для любого ε>0 существует b в s с a ≤ b < a+ε.

LaTeX

$$$\forall s,a,\varepsilon>0,\ IsGLB(s,a) \Rightarrow \exists b\in s:\ a \le b \land b < a+\varepsilon$$$

Lean4

theorem exists_between_self_add (h : IsGLB s a) (hε : 0 < ε) : ∃ b ∈ s, a ≤ b ∧ b < a + ε :=
  h.exists_between <| lt_add_of_pos_right _ hε

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