Theorems · Theorem · order theory

mul_ciSup_le

∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Group α] [MulLeftMono α]
  {a g : α} {h : ι → α}, (∀ (j : ι), g * h j ≤ a) → g * iSup h ≤ a

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Group

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

NonemptyConditionallyCompleteLatticeGroupMulLeftMono