Bounds on scalar multiplication of set #
This file proves order properties of pointwise operations of sets.
theorem
smul_lowerBounds_subset_lowerBounds_smul_of_nonneg
{α : Type u_1}
{β : Type u_2}
[SMul α β]
[Preorder α]
[Preorder β]
[Zero α]
[PosSMulMono α β]
{a : α}
{s : Set β}
(ha : 0 ≤ a)
:
a • lowerBounds s ⊆ lowerBounds (a • s)
theorem
smul_upperBounds_subset_upperBounds_smul_of_nonneg
{α : Type u_1}
{β : Type u_2}
[SMul α β]
[Preorder α]
[Preorder β]
[Zero α]
[PosSMulMono α β]
{a : α}
{s : Set β}
(ha : 0 ≤ a)
:
a • upperBounds s ⊆ upperBounds (a • s)
theorem
BddBelow.smul_of_nonneg
{α : Type u_1}
{β : Type u_2}
[SMul α β]
[Preorder α]
[Preorder β]
[Zero α]
[PosSMulMono α β]
{a : α}
{s : Set β}
(hs : BddBelow s)
(ha : 0 ≤ a)
:
BddBelow (a • s)
theorem
BddAbove.smul_of_nonneg
{α : Type u_1}
{β : Type u_2}
[SMul α β]
[Preorder α]
[Preorder β]
[Zero α]
[PosSMulMono α β]
{a : α}
{s : Set β}
(hs : BddAbove s)
(ha : 0 ≤ a)
:
BddAbove (a • s)
@[simp]
theorem
lowerBounds_smul_of_pos
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[GroupWithZero α]
[Zero β]
[MulActionWithZero α β]
[PosSMulMono α β]
[PosSMulReflectLE α β]
{s : Set β}
{a : α}
(ha : 0 < a)
:
lowerBounds (a • s) = a • lowerBounds s
@[simp]
theorem
upperBounds_smul_of_pos
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[GroupWithZero α]
[Zero β]
[MulActionWithZero α β]
[PosSMulMono α β]
[PosSMulReflectLE α β]
{s : Set β}
{a : α}
(ha : 0 < a)
:
upperBounds (a • s) = a • upperBounds s
@[simp]
theorem
bddBelow_smul_iff_of_pos
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[GroupWithZero α]
[Zero β]
[MulActionWithZero α β]
[PosSMulMono α β]
[PosSMulReflectLE α β]
{s : Set β}
{a : α}
(ha : 0 < a)
:
@[simp]
theorem
bddAbove_smul_iff_of_pos
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[GroupWithZero α]
[Zero β]
[MulActionWithZero α β]
[PosSMulMono α β]
[PosSMulReflectLE α β]
{s : Set β}
{a : α}
(ha : 0 < a)
:
theorem
smul_lowerBounds_subset_upperBounds_smul
{α : Type u_1}
{β : Type u_2}
[Ring α]
[PartialOrder α]
[IsOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a ≤ 0)
:
a • lowerBounds s ⊆ upperBounds (a • s)
theorem
smul_upperBounds_subset_lowerBounds_smul
{α : Type u_1}
{β : Type u_2}
[Ring α]
[PartialOrder α]
[IsOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a ≤ 0)
:
a • upperBounds s ⊆ lowerBounds (a • s)
theorem
BddBelow.smul_of_nonpos
{α : Type u_1}
{β : Type u_2}
[Ring α]
[PartialOrder α]
[IsOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a ≤ 0)
(hs : BddBelow s)
:
BddAbove (a • s)
theorem
BddAbove.smul_of_nonpos
{α : Type u_1}
{β : Type u_2}
[Ring α]
[PartialOrder α]
[IsOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a ≤ 0)
(hs : BddAbove s)
:
BddBelow (a • s)
@[simp]
theorem
lowerBounds_smul_of_neg
{α : Type u_1}
{β : Type u_2}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a < 0)
:
lowerBounds (a • s) = a • upperBounds s
@[simp]
theorem
upperBounds_smul_of_neg
{α : Type u_1}
{β : Type u_2}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a < 0)
:
upperBounds (a • s) = a • lowerBounds s
@[simp]
theorem
bddBelow_smul_iff_of_neg
{α : Type u_1}
{β : Type u_2}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a < 0)
:
@[simp]
theorem
bddAbove_smul_iff_of_neg
{α : Type u_1}
{β : Type u_2}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
[Module α β]
[PosSMulMono α β]
{s : Set β}
{a : α}
(ha : a < 0)
: