Mathlib.Data.Real.Pointwise

Real.sInf_smul_of_nonneg theorem

(ha : 0 ≤ a) (s : Set ℝ) : sInf (a • s) = a • sInf s

Full source

theorem Real.sInf_smul_of_nonneg (ha : 0 ≤ a) (s : Set ℝ) : sInf (a • s) = a • sInf s := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · rw [smul_set_empty, Real.sInf_empty, smul_zero]
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_smul_set hs, zero_smul]
    exact csInf_singleton 0
  by_cases h : BddBelow s
  · exact ((OrderIso.smulRight ha').map_csInf' hs h).symm
  · rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]

Infimum of Scaled Set Equals Scaled Infimum for Nonnegative $a$

Informal description

For any nonnegative real number $a \geq 0$ and any set $s \subseteq \mathbb{R}$, the infimum of the scaled set $a \cdot s$ equals $a$ times the infimum of $s$, i.e., \[ \inf (a \cdot s) = a \cdot \inf s. \]

Real.smul_iInf_of_nonneg theorem

(ha : 0 ≤ a) (f : ι → ℝ) : (a • ⨅ i, f i) = ⨅ i, a • f i

Full source

theorem Real.smul_iInf_of_nonneg (ha : 0 ≤ a) (f : ι → ℝ) : (a • ⨅ i, f i) = ⨅ i, a • f i :=
  (Real.sInf_smul_of_nonneg ha _).symm.trans <| congr_arg sInf <| (range_comp _ _).symm

Scalar Multiplication Distributes over Infimum for Nonnegative Scalars: $a \cdot \bigwedge_i f_i = \bigwedge_i (a \cdot f_i)$

Informal description

For any nonnegative real number $a \geq 0$ and any family of real numbers $(f_i)_{i \in \iota}$, the scalar multiplication of $a$ with the infimum of the family equals the infimum of the scaled family, i.e., \[ a \cdot \left(\bigwedge_{i} f_i\right) = \bigwedge_{i} (a \cdot f_i). \]

Real.sSup_smul_of_nonneg theorem

(ha : 0 ≤ a) (s : Set ℝ) : sSup (a • s) = a • sSup s

Full source

theorem Real.sSup_smul_of_nonneg (ha : 0 ≤ a) (s : Set ℝ) : sSup (a • s) = a • sSup s := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · rw [smul_set_empty, Real.sSup_empty, smul_zero]
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0
  by_cases h : BddAbove s
  · exact ((OrderIso.smulRight ha').map_csSup' hs h).symm
  · rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]

Supremum of Scaled Set: $\sup (a \cdot s) = a \cdot \sup s$ for $a \geq 0$

Informal description

For any nonnegative real number $a \geq 0$ and any set $s \subseteq \mathbb{R}$, the supremum of the scaled set $a \cdot s$ is equal to $a$ times the supremum of $s$, i.e., \[ \sup (a \cdot s) = a \cdot \sup s. \]

Real.smul_iSup_of_nonneg theorem

(ha : 0 ≤ a) (f : ι → ℝ) : (a • ⨆ i, f i) = ⨆ i, a • f i

Full source

theorem Real.smul_iSup_of_nonneg (ha : 0 ≤ a) (f : ι → ℝ) : (a • ⨆ i, f i) = ⨆ i, a • f i :=
  (Real.sSup_smul_of_nonneg ha _).symm.trans <| congr_arg sSup <| (range_comp _ _).symm

Supremum Commutes with Nonnegative Scalar Multiplication: $a \cdot \sup_i f_i = \sup_i (a \cdot f_i)$ for $a \geq 0$

Informal description

For any nonnegative real number $a \geq 0$ and any family of real numbers $(f_i)_{i \in \iota}$, the scalar multiplication of $a$ with the supremum of the family equals the supremum of the scalar multiples, i.e., \[ a \cdot \left(\sup_{i} f_i\right) = \sup_{i} (a \cdot f_i). \]

Real.sInf_smul_of_nonpos theorem

(ha : a ≤ 0) (s : Set ℝ) : sInf (a • s) = a • sSup s

Full source

theorem Real.sInf_smul_of_nonpos (ha : a ≤ 0) (s : Set ℝ) : sInf (a • s) = a • sSup s := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · rw [smul_set_empty, Real.sInf_empty, Real.sSup_empty, smul_zero]
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_smul_set hs, zero_smul]
    exact csInf_singleton 0
  by_cases h : BddAbove s
  · exact ((OrderIso.smulRightDual ℝ ha').map_csSup' hs h).symm
  · rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_neg ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]

Infimum of Scaled Set by Nonpositive Scalar Equals Scalar Times Supremum

Informal description

For any real number $a \leq 0$ and any set $s$ of real numbers, the infimum of the scaled set $a \cdot s$ is equal to $a$ times the supremum of $s$, i.e., $\inf (a \cdot s) = a \cdot \sup s$.

Real.smul_iSup_of_nonpos theorem

(ha : a ≤ 0) (f : ι → ℝ) : (a • ⨆ i, f i) = ⨅ i, a • f i

Full source

theorem Real.smul_iSup_of_nonpos (ha : a ≤ 0) (f : ι → ℝ) : (a • ⨆ i, f i) = ⨅ i, a • f i :=
  (Real.sInf_smul_of_nonpos ha _).symm.trans <| congr_arg sInf <| (range_comp _ _).symm

Scalar Multiplication of Supremum by Nonpositive Real Equals Infimum of Scalar Multiples: $a \cdot (\sup_i f_i) = \inf_i (a \cdot f_i)$ for $a \leq 0$

Informal description

For any real number $a \leq 0$ and any indexed family of real numbers $(f_i)_{i \in \iota}$, the scalar multiplication of $a$ with the supremum of the family equals the infimum of the scalar multiples: \[ a \cdot \left(\bigsqcup_{i} f_i\right) = \bigsqcap_{i} (a \cdot f_i). \]

Real.sSup_smul_of_nonpos theorem

(ha : a ≤ 0) (s : Set ℝ) : sSup (a • s) = a • sInf s

Full source

theorem Real.sSup_smul_of_nonpos (ha : a ≤ 0) (s : Set ℝ) : sSup (a • s) = a • sInf s := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0
  by_cases h : BddBelow s
  · exact ((OrderIso.smulRightDual ℝ ha').map_csInf' hs h).symm
  · rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_neg ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]

Supremum of Scaled Set for Nonpositive Scalars: $\sup (a \cdot s) = a \cdot \inf s$ when $a \leq 0$

Informal description

For any real number $a \leq 0$ and any set $s$ of real numbers, the supremum of the scaled set $a \cdot s$ equals $a$ times the infimum of $s$, i.e., \[ \sup (a \cdot s) = a \cdot \inf s. \]

Real.smul_iInf_of_nonpos theorem

(ha : a ≤ 0) (f : ι → ℝ) : (a • ⨅ i, f i) = ⨆ i, a • f i

Full source

theorem Real.smul_iInf_of_nonpos (ha : a ≤ 0) (f : ι → ℝ) : (a • ⨅ i, f i) = ⨆ i, a • f i :=
  (Real.sSup_smul_of_nonpos ha _).symm.trans <| congr_arg sSup <| (range_comp _ _).symm

Scalar Multiplication of Infimum by Nonpositive Real Equals Supremum of Scalar Multiplications: $a \cdot (\bigwedge_i f_i) = \bigvee_i (a \cdot f_i)$ for $a \leq 0$

Informal description

For any real number $a \leq 0$ and any indexed family of real numbers $(f_i)_{i \in \iota}$, the scalar multiplication of $a$ with the infimum of the family equals the supremum of the scalar multiplications, i.e., \[ a \cdot \left(\bigwedge_{i} f_i\right) = \bigvee_{i} (a \cdot f_i). \]

Real.mul_iInf_of_nonneg theorem

(ha : 0 ≤ r) (f : ι → ℝ) : (r * ⨅ i, f i) = ⨅ i, r * f i

Full source

theorem Real.mul_iInf_of_nonneg (ha : 0 ≤ r) (f : ι → ℝ) : (r * ⨅ i, f i) = ⨅ i, r * f i :=
  Real.smul_iInf_of_nonneg ha f

Multiplication by Nonnegative Real Distributes over Infimum: $r \cdot \bigwedge_i f_i = \bigwedge_i (r \cdot f_i)$ for $r \geq 0$

Informal description

For any nonnegative real number $r \geq 0$ and any family of real numbers $(f_i)_{i \in \iota}$, the product of $r$ with the infimum of the family equals the infimum of the products, i.e., \[ r \cdot \left(\bigwedge_{i} f_i\right) = \bigwedge_{i} (r \cdot f_i). \]

Real.mul_iSup_of_nonneg theorem

(ha : 0 ≤ r) (f : ι → ℝ) : (r * ⨆ i, f i) = ⨆ i, r * f i

Full source

theorem Real.mul_iSup_of_nonneg (ha : 0 ≤ r) (f : ι → ℝ) : (r * ⨆ i, f i) = ⨆ i, r * f i :=
  Real.smul_iSup_of_nonneg ha f

Multiplication Commutes with Supremum for Nonnegative Reals: $r \cdot \sup_i f_i = \sup_i (r \cdot f_i)$ for $r \geq 0$

Informal description

For any nonnegative real number $r \geq 0$ and any family of real numbers $(f_i)_{i \in \iota}$, the product of $r$ with the supremum of the family equals the supremum of the products, i.e., \[ r \cdot \left(\sup_{i} f_i\right) = \sup_{i} (r \cdot f_i). \]

Real.mul_iInf_of_nonpos theorem

(ha : r ≤ 0) (f : ι → ℝ) : (r * ⨅ i, f i) = ⨆ i, r * f i

Full source

theorem Real.mul_iInf_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (r * ⨅ i, f i) = ⨆ i, r * f i :=
  Real.smul_iInf_of_nonpos ha f

Product of Nonpositive Real and Infimum Equals Supremum of Products

Informal description

For any real number $r \leq 0$ and any indexed family of real numbers $(f_i)_{i \in \iota}$, the product of $r$ with the infimum of the family equals the supremum of the products, i.e., \[ r \cdot \left(\bigwedge_{i} f_i\right) = \bigvee_{i} (r \cdot f_i). \]

Real.mul_iSup_of_nonpos theorem

(ha : r ≤ 0) (f : ι → ℝ) : (r * ⨆ i, f i) = ⨅ i, r * f i

Full source

theorem Real.mul_iSup_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (r * ⨆ i, f i) = ⨅ i, r * f i :=
  Real.smul_iSup_of_nonpos ha f

Multiplication of Supremum by Nonpositive Real Equals Infimum of Products: $r \cdot (\sup_i f_i) = \inf_i (r \cdot f_i)$ for $r \leq 0$

Informal description

For any real number $r \leq 0$ and any indexed family of real numbers $(f_i)_{i \in \iota}$, the product of $r$ with the supremum of the family equals the infimum of the products: \[ r \cdot \left(\bigsqcup_{i} f_i\right) = \bigsqcap_{i} (r \cdot f_i). \]

Real.iInf_mul_of_nonneg theorem

(ha : 0 ≤ r) (f : ι → ℝ) : (⨅ i, f i) * r = ⨅ i, f i * r

Full source

theorem Real.iInf_mul_of_nonneg (ha : 0 ≤ r) (f : ι → ℝ) : (⨅ i, f i) * r = ⨅ i, f i * r := by
  simp only [Real.mul_iInf_of_nonneg ha, mul_comm]

Infimum-Multiplication Commutation for Nonnegative Reals: $(\inf_i f_i) \cdot r = \inf_i (f_i \cdot r)$ when $r \geq 0$

Informal description

For any nonnegative real number $r \geq 0$ and any family of real numbers $(f_i)_{i \in \iota}$, the product of the infimum of the family with $r$ equals the infimum of the products, i.e., \[ \left(\bigwedge_{i} f_i\right) \cdot r = \bigwedge_{i} (f_i \cdot r). \]

Real.iSup_mul_of_nonneg theorem

(ha : 0 ≤ r) (f : ι → ℝ) : (⨆ i, f i) * r = ⨆ i, f i * r

Full source

theorem Real.iSup_mul_of_nonneg (ha : 0 ≤ r) (f : ι → ℝ) : (⨆ i, f i) * r = ⨆ i, f i * r := by
  simp only [Real.mul_iSup_of_nonneg ha, mul_comm]

Supremum-Multiplication Commutation for Nonnegative Reals: $(\sup_i f_i) \cdot r = \sup_i (f_i \cdot r)$ when $r \geq 0$

Informal description

For any nonnegative real number $r \geq 0$ and any family of real numbers $(f_i)_{i \in \iota}$, the product of the supremum of the family with $r$ equals the supremum of the products, i.e., \[ \left(\sup_{i} f_i\right) \cdot r = \sup_{i} (f_i \cdot r). \]

Real.iInf_mul_of_nonpos theorem

(ha : r ≤ 0) (f : ι → ℝ) : (⨅ i, f i) * r = ⨆ i, f i * r

Full source

theorem Real.iInf_mul_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (⨅ i, f i) * r = ⨆ i, f i * r := by
  simp only [Real.mul_iInf_of_nonpos ha, mul_comm]

Infimum-Multiplication Identity for Nonpositive Reals: $(\inf_i f_i) \cdot r = \sup_i (f_i \cdot r)$ when $r \leq 0$

Informal description

For any real number $r \leq 0$ and any indexed family of real numbers $(f_i)_{i \in \iota}$, the product of the infimum of the family with $r$ equals the supremum of the products of $r$ with each $f_i$, i.e., \[ \left(\bigwedge_{i} f_i\right) \cdot r = \bigvee_{i} (f_i \cdot r). \]

Real.iSup_mul_of_nonpos theorem

(ha : r ≤ 0) (f : ι → ℝ) : (⨆ i, f i) * r = ⨅ i, f i * r

Full source

theorem Real.iSup_mul_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (⨆ i, f i) * r = ⨅ i, f i * r := by
  simp only [Real.mul_iSup_of_nonpos ha, mul_comm]

Supremum multiplied by nonpositive real equals infimum of products: $(\sup_i f_i) \cdot r = \inf_i (f_i \cdot r)$ for $r \leq 0$

Informal description

For any real number $r \leq 0$ and any indexed family of real numbers $(f_i)_{i \in \iota}$, the product of the supremum of the family with $r$ equals the infimum of the products: \[ \left(\bigsqcup_{i} f_i\right) \cdot r = \bigsqcap_{i} (f_i \cdot r). \]

TODO