exists_between_sub_self — Mathlib

English

If s has a least upper bound a, then for any ε>0 there exists b ∈ s with a-ε < b ≤ a.

Русский

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

LaTeX

$$$\forall s,a,\varepsilon>0,\ IsLUB(s,a) \Rightarrow \exists b\in s,\ a-\varepsilon < b \land b \le a$$$

Lean4

theorem exists_between_sub_self (h : IsLUB s a) (hε : 0 < ε) : ∃ b ∈ s, a - ε < b ∧ b ≤ a :=
  h.exists_between <| sub_lt_self _ hε

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