Theorems · Theorem · order theory

IsLUB.add

∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G},
  IsLUB s a → IsLUB t b → IsLUB (s + t) (a + b)

Defined in

Mathlib.Algebra.Order.Group.Pointwise.Bounds

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupPreorderAddLeftMonoAddRightMono