# 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 α β] [] [] [Zero α] [] {a : α} {s : Set β} (ha : 0 a) :
theorem smul_upperBounds_subset_upperBounds_smul_of_nonneg {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [] {a : α} {s : Set β} (ha : 0 a) :
theorem BddBelow.smul_of_nonneg {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [] {a : α} {s : Set β} (hs : ) (ha : 0 a) :
theorem BddAbove.smul_of_nonneg {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [] {a : α} {s : Set β} (hs : ) (ha : 0 a) :
@[simp]
theorem lowerBounds_smul_of_pos {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] [] [] [] {s : Set β} {a : α} (ha : 0 < a) :
lowerBounds (a s) = a
@[simp]
theorem upperBounds_smul_of_pos {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] [] [] [] {s : Set β} {a : α} (ha : 0 < a) :
upperBounds (a s) = a
@[simp]
theorem bddBelow_smul_iff_of_pos {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] [] [] [] {s : Set β} {a : α} (ha : 0 < a) :
@[simp]
theorem bddAbove_smul_iff_of_pos {α : Type u_1} {β : Type u_2} [] [] [] [Zero β] [] [] [] {s : Set β} {a : α} (ha : 0 < a) :
theorem smul_lowerBounds_subset_upperBounds_smul {α : Type u_1} {β : Type u_2} [] [Module α β] [] {s : Set β} {a : α} (ha : a 0) :
theorem smul_upperBounds_subset_lowerBounds_smul {α : Type u_1} {β : Type u_2} [] [Module α β] [] {s : Set β} {a : α} (ha : a 0) :
theorem BddBelow.smul_of_nonpos {α : Type u_1} {β : Type u_2} [] [Module α β] [] {s : Set β} {a : α} (ha : a 0) (hs : ) :
theorem BddAbove.smul_of_nonpos {α : Type u_1} {β : Type u_2} [] [Module α β] [] {s : Set β} {a : α} (ha : a 0) (hs : ) :
@[simp]
theorem lowerBounds_smul_of_neg {α : Type u_1} {β : Type u_2} [Module α β] [] {s : Set β} {a : α} (ha : a < 0) :
lowerBounds (a s) = a
@[simp]
theorem upperBounds_smul_of_neg {α : Type u_1} {β : Type u_2} [Module α β] [] {s : Set β} {a : α} (ha : a < 0) :
upperBounds (a s) = a
@[simp]
theorem bddBelow_smul_iff_of_neg {α : Type u_1} {β : Type u_2} [Module α β] [] {s : Set β} {a : α} (ha : a < 0) :
@[simp]
theorem bddAbove_smul_iff_of_neg {α : Type u_1} {β : Type u_2} [Module α β] [] {s : Set β} {a : α} (ha : a < 0) :