theorem
BddAbove.range_comp_of_nonneg
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Nonempty α]
[Preorder β]
[Zero β]
[Preorder γ]
{f : α → β}
{g : β → γ}
(hf : BddAbove (Set.range f))
(hf0 : 0 ≤ f)
(hg : MonotoneOn g {x : β | 0 ≤ x})
:
A variant of BddAbove.range_comp that assumes that f is nonnegative and g is monotone on
nonnegative values.
theorem
bddAbove_range_mul
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
{u v : α → β}
[Preorder β]
[Zero β]
[Mul β]
[PosMulMono β]
[MulPosMono β]
(hu : BddAbove (Set.range u))
(hu0 : 0 ≤ u)
(hv : BddAbove (Set.range v))
(hv0 : 0 ≤ v)
:
If u v : α → β are nonnegative and bounded above, then u * v is bounded above.