exists_between_self_add' — Mathlib

English

If a is the GLB of s and a ∉ s, then there exists b ∈ s with a < b < a+ε for every ε>0.

Русский

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

LaTeX

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

Lean4

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

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