English
Let a ≤ 0 and S be a subset of ℝ. Then the supremum of a·S equals a times the infimum of S: sSup(a·S) = a·sInf(S).
Русский
Пусть a ≤ 0 и S ⊆ ℝ. Тогда sSup(a·S) = a·sInf(S).
LaTeX
$$$ \operatorname{sSup}(a \cdot S) = a \cdot \operatorname{sInf}(S) $$$
Lean4
theorem 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]
