sInf_smul_of_nonpos — Mathlib

English

For a ≤ 0, sInf(a · S) = a · sInf S.

Русский

Для a ≤ 0 выполняется sInf(a · S) = a · sInf S.

LaTeX

$$$ a \le 0 \Rightarrow sInf(a \cdot S) = a \cdot sInf S $$$

Lean4

theorem 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]

Похожие утверждения