Theorems · Theorem · order theory

le_ciInf_mul_ciInf

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

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Group

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonemptyNonemptyConditionallyCompleteLatticeGroupMulLeftMonoMulRightMono