exists_between_sub_self'

Mathlib.Algebra.Order.Group.Bounds

URI: https://scilib.ai/kg/mathlib#IsLUB.exists_between_sub_self'

English

If s has GLB a and a ∉ s, then there exists b ∈ s with a-ε < b < a.

Русский

Если s имеет границу снизу a и a ∉ s, существует b ∈ s: a-ε < b < a.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru