Theorems · Theorem · order theory

IsLUB.exists_between_sub_self

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {s : Set α} {a ε : α},
  IsLUB s a → 0 < ε → ∃ b ∈ s, a - ε < b ∧ b ≤ a

Defined in

Mathlib.Algebra.Order.Group.Bounds

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoid