Mathlib.Algebra.Order.Module.Pointwise

smul_lowerBounds_subset_lowerBounds_smul_of_nonneg theorem

(ha : 0 ≤ a) : a • lowerBounds s ⊆ lowerBounds (a • s)

Full source

lemma smul_lowerBounds_subset_lowerBounds_smul_of_nonneg (ha : 0 ≤ a) :
    a • lowerBounds s ⊆ lowerBounds (a • s) :=
  (monotone_smul_left_of_nonneg ha).image_lowerBounds_subset_lowerBounds_image

Inclusion of Scalar Multiples of Lower Bounds for Nonnegative Scalars

Informal description

For any scalar $a \geq 0$, the scalar multiplication of the lower bounds of a set $s$ is contained in the lower bounds of the scalar multiplication of $s$, i.e., $a \cdot \text{lowerBounds}(s) \subseteq \text{lowerBounds}(a \cdot s)$.

smul_upperBounds_subset_upperBounds_smul_of_nonneg theorem

(ha : 0 ≤ a) : a • upperBounds s ⊆ upperBounds (a • s)

Full source

lemma smul_upperBounds_subset_upperBounds_smul_of_nonneg (ha : 0 ≤ a) :
    a • upperBounds s ⊆ upperBounds (a • s) :=
  (monotone_smul_left_of_nonneg ha).image_upperBounds_subset_upperBounds_image

Scalar Multiplication Preserves Upper Bounds for Nonnegative Scalars

Informal description

For any real number $a \geq 0$ and any set $s$ in a real vector space, the scalar multiple $a \cdot \text{upperBounds}(s)$ is contained in the set of upper bounds of the scalar multiple $a \cdot s$.

BddBelow.smul_of_nonneg theorem

(hs : BddBelow s) (ha : 0 ≤ a) : BddBelow (a • s)

Full source

lemma BddBelow.smul_of_nonneg (hs : BddBelow s) (ha : 0 ≤ a) : BddBelow (a • s) :=
  (monotone_smul_left_of_nonneg ha).map_bddBelow hs

Nonnegative Scalar Multiplication Preserves Lower Boundedness

Informal description

If a set $s$ is bounded below and $a \geq 0$ is a nonnegative scalar, then the scalar multiple $a \cdot s$ is also bounded below.

BddAbove.smul_of_nonneg theorem

(hs : BddAbove s) (ha : 0 ≤ a) : BddAbove (a • s)

Full source

lemma BddAbove.smul_of_nonneg (hs : BddAbove s) (ha : 0 ≤ a) : BddAbove (a • s) :=
  (monotone_smul_left_of_nonneg ha).map_bddAbove hs

Nonnegative Scalar Multiplication Preserves Boundedness Above

Informal description

For any set $s$ in a real vector space that is bounded above, and for any nonnegative real number $a \geq 0$, the scalar multiple $a \cdot s$ is also bounded above.

lowerBounds_smul_of_pos theorem

(ha : 0 < a) : lowerBounds (a • s) = a • lowerBounds s

Full source

@[simp] lemma lowerBounds_smul_of_pos (ha : 0 < a) : lowerBounds (a • s) = a • lowerBounds s :=
  (OrderIso.smulRight ha).lowerBounds_image

Scalar Multiplication Preserves Lower Bounds for Positive Scalars

Informal description

For a positive scalar $a > 0$, the set of lower bounds of the scaled set $a \cdot s$ is equal to the scaled set of lower bounds of $s$, i.e., $\text{lowerBounds}(a \cdot s) = a \cdot \text{lowerBounds}(s)$.

upperBounds_smul_of_pos theorem

(ha : 0 < a) : upperBounds (a • s) = a • upperBounds s

Full source

@[simp] lemma upperBounds_smul_of_pos (ha : 0 < a) : upperBounds (a • s) = a • upperBounds s :=
  (OrderIso.smulRight ha).upperBounds_image

Upper bounds of scaled set under positive scalar multiplication

Informal description

For a positive scalar $a > 0$, the set of upper bounds of the scaled set $a \cdot s$ is equal to the scaled set of upper bounds of $s$, i.e., $\text{upperBounds}(a \cdot s) = a \cdot \text{upperBounds}(s)$.

bddBelow_smul_iff_of_pos theorem

(ha : 0 < a) : BddBelow (a • s) ↔ BddBelow s

Full source

@[simp] lemma bddBelow_smul_iff_of_pos (ha : 0 < a) : BddBelowBddBelow (a • s) ↔ BddBelow s :=
  (OrderIso.smulRight ha).bddBelow_image

Bounded Below Condition for Positive Scalar Multiplication: $a \cdot s$ is bounded below iff $s$ is bounded below ($a > 0$)

Informal description

For a positive scalar $a > 0$, the set $a \cdot s$ is bounded below if and only if the set $s$ is bounded below.

bddAbove_smul_iff_of_pos theorem

(ha : 0 < a) : BddAbove (a • s) ↔ BddAbove s

Full source

@[simp] lemma bddAbove_smul_iff_of_pos (ha : 0 < a) : BddAboveBddAbove (a • s) ↔ BddAbove s :=
  (OrderIso.smulRight ha).bddAbove_image

Boundedness under positive scalar multiplication: $a \cdot s$ is bounded above iff $s$ is bounded above ($a > 0$)

Informal description

For a positive scalar $a > 0$ and a set $s$ in a real vector space, the set $a \cdot s$ is bounded above if and only if $s$ is bounded above.

smul_lowerBounds_subset_upperBounds_smul theorem

(ha : a ≤ 0) : a • lowerBounds s ⊆ upperBounds (a • s)

Full source

lemma smul_lowerBounds_subset_upperBounds_smul (ha : a ≤ 0) :
    a • lowerBounds s ⊆ upperBounds (a • s) :=
  (antitone_smul_left ha).image_lowerBounds_subset_upperBounds_image

Inclusion of Scalar Multiplication of Lower Bounds into Upper Bounds for Nonpositive Scalars

Informal description

For any scalar $a \leq 0$, the scalar multiplication of the lower bounds of a set $s$ is contained in the upper bounds of the scalar multiplication of $s$, i.e., $$ a \cdot \text{lowerBounds}(s) \subseteq \text{upperBounds}(a \cdot s). $$

smul_upperBounds_subset_lowerBounds_smul theorem

(ha : a ≤ 0) : a • upperBounds s ⊆ lowerBounds (a • s)

Full source

lemma smul_upperBounds_subset_lowerBounds_smul (ha : a ≤ 0) :
    a • upperBounds s ⊆ lowerBounds (a • s) :=
  (antitone_smul_left ha).image_upperBounds_subset_lowerBounds_image

Inclusion of Scalar Multiples of Upper Bounds into Lower Bounds for Nonpositive Scalars

Informal description

For any real number $a \leq 0$ and any set $s$ in a real vector space, the scalar multiple $a \cdot \text{upperBounds}(s)$ is a subset of the lower bounds of the scalar multiple $a \cdot s$.

BddBelow.smul_of_nonpos theorem

(ha : a ≤ 0) (hs : BddBelow s) : BddAbove (a • s)

Full source

lemma BddBelow.smul_of_nonpos (ha : a ≤ 0) (hs : BddBelow s) : BddAbove (a • s) :=
  (antitone_smul_left ha).map_bddBelow hs

Scalar multiplication by nonpositive preserves boundedness from below to above

Informal description

For any scalar $a \leq 0$ and any set $s$ that is bounded below, the set $a \cdot s$ is bounded above.

BddAbove.smul_of_nonpos theorem

(ha : a ≤ 0) (hs : BddAbove s) : BddBelow (a • s)

Full source

lemma BddAbove.smul_of_nonpos (ha : a ≤ 0) (hs : BddAbove s) : BddBelow (a • s) :=
  (antitone_smul_left ha).map_bddAbove hs

Scalar multiplication by nonpositive preserves boundedness from above to below

Informal description

For any scalar $a \leq 0$ and any set $s$ that is bounded above, the set $a \cdot s$ is bounded below.

lowerBounds_smul_of_neg theorem

(ha : a < 0) : lowerBounds (a • s) = a • upperBounds s

Full source

@[simp] lemma lowerBounds_smul_of_neg (ha : a < 0) : lowerBounds (a • s) = a • upperBounds s :=
  (OrderIso.smulRightDual β ha).upperBounds_image

Lower bounds of negatively scaled set equals negative scaling of upper bounds

Informal description

For a real number $a < 0$ and a set $s$ in a real vector space, the set of lower bounds of the scaled set $a \cdot s$ is equal to the scaled set $a \cdot \text{upperBounds}(s)$. That is, $\text{lowerBounds}(a \cdot s) = a \cdot \text{upperBounds}(s)$.

upperBounds_smul_of_neg theorem

(ha : a < 0) : upperBounds (a • s) = a • lowerBounds s

Full source

@[simp] lemma upperBounds_smul_of_neg (ha : a < 0) : upperBounds (a • s) = a • lowerBounds s :=
  (OrderIso.smulRightDual β ha).lowerBounds_image

Upper Bounds of Negatively Scaled Set Equals Scaled Lower Bounds

Informal description

For a negative scalar $a < 0$ and a set $s$ in an ordered vector space, the set of upper bounds of the scaled set $a \cdot s$ is equal to the scaled set of lower bounds of $s$, i.e., \[ \text{upperBounds}(a \cdot s) = a \cdot \text{lowerBounds}(s). \]

bddBelow_smul_iff_of_neg theorem

(ha : a < 0) : BddBelow (a • s) ↔ BddAbove s

Full source

@[simp] lemma bddBelow_smul_iff_of_neg (ha : a < 0) : BddBelowBddBelow (a • s) ↔ BddAbove s :=
  (OrderIso.smulRightDual β ha).bddAbove_image

Bounded Below Scalar Multiplication of Set by Negative Scalar is Equivalent to Bounded Above Original Set

Informal description

For a real number $a < 0$ and a set $s$ in a real vector space, the set $a \cdot s$ is bounded below if and only if $s$ is bounded above.

bddAbove_smul_iff_of_neg theorem

(ha : a < 0) : BddAbove (a • s) ↔ BddBelow s

Full source

@[simp] lemma bddAbove_smul_iff_of_neg (ha : a < 0) : BddAboveBddAbove (a • s) ↔ BddBelow s :=
  (OrderIso.smulRightDual β ha).bddBelow_image

Boundedness of Scalar Multiplication for Negative Scalars: $a < 0 \implies (\text{BddAbove}(a \cdot s) \leftrightarrow \text{BddBelow}(s))$

Informal description

For a scalar $a < 0$ and a set $s$ in a real vector space, the set $a \cdot s$ is bounded above if and only if $s$ is bounded below.