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) : BddBelow (a • s) ↔ BddBelow s

@[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) : BddAbove (a • s) ↔ BddAbove s

theorem smul_lowerBounds_subset_upperBounds_smul {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [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} [OrderedRing α] [OrderedAddCommGroup β] [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} [OrderedRing α] [OrderedAddCommGroup β] [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} [OrderedRing α] [OrderedAddCommGroup β] [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} [LinearOrderedField α] [OrderedAddCommGroup β] [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} [LinearOrderedField α] [OrderedAddCommGroup β] [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} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {s : Set β} {a : α} (ha : a < 0) : BddBelow (a • s) ↔ BddAbove s

@[simp]

theorem bddAbove_smul_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {s : Set β} {a : α} (ha : a < 0) : BddAbove (a • s) ↔ BddBelow s