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

ink

theorem IsGLB.exists_between_self_add {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {s : Set α} {a : α} {ε : α} (h : IsGLB s a) (hε : 0 < ε) : ∃ b, b ∈ s ∧ a ≤ b ∧ b < a + ε

ink

theorem IsGLB.exists_between_self_add' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {s : Set α} {a : α} {ε : α} (h : IsGLB s a) (h₂ : ¬a ∈ s) (hε : 0 < ε) : ∃ b, b ∈ s ∧ a < b ∧ b < a + ε

ink

theorem IsLUB.exists_between_sub_self {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {s : Set α} {a : α} {ε : α} (h : IsLUB s a) (hε : 0 < ε) : ∃ b, b ∈ s ∧ a - ε < b ∧ b ≤ a

ink

theorem IsLUB.exists_between_sub_self' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {s : Set α} {a : α} {ε : α} (h : IsLUB s a) (h₂ : ¬a ∈ s) (hε : 0 < ε) : ∃ b, b ∈ s ∧ a - ε < b ∧ b < a