Documentation

Mathlib.Algebra.Order.Group.Bounds

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

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