English
If a ≥ 0, then sInf(a · S) = a · sInf S for a set S of real numbers.
Русский
Если a ≥ 0, то sInf(a · S) = a · sInf S для множества S вещественных чисел.
LaTeX
$$$ (0 \le a) \Rightarrow sInf(a \cdot S) = a \cdot sInf S $$$
Lean4
theorem 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]
