Theorems · Theorem · order theory

BddAbove.range_mul

∀ {ι : Type u_1} {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {f g : ι → M},
  BddAbove (Set.range f) → BddAbove (Set.range g) → BddAbove (Set.range fun i => f i * g i)

Defined in

Mathlib.Algebra.Order.Group.Pointwise.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

MulPreorderMulLeftMonoMulRightMono