Least upper bound and the greatest lower bound in linear ordered additive commutative groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem is_glb.exists_between_self_add {α : Type u_1} [linear_ordered_add_comm_group α] {s : set α} {a ε : α} (h : is_glb s a) (hε : 0 < ε) :

∃ (b : α) (H : b ∈ s), a ≤ b ∧ b < a + ε

theorem is_glb.exists_between_self_add' {α : Type u_1} [linear_ordered_add_comm_group α] {s : set α} {a ε : α} (h : is_glb s a) (h₂ : a ∉ s) (hε : 0 < ε) :

∃ (b : α) (H : b ∈ s), a < b ∧ b < a + ε

theorem is_lub.exists_between_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] {s : set α} {a ε : α} (h : is_lub s a) (hε : 0 < ε) :

∃ (b : α) (H : b ∈ s), a - ε < b ∧ b ≤ a

theorem is_lub.exists_between_sub_self' {α : Type u_1} [linear_ordered_add_comm_group α] {s : set α} {a ε : α} (h : is_lub s a) (h₂ : a ∉ s) (hε : 0 < ε) :

∃ (b : α) (H : b ∈ s), a - ε < b ∧ b < a