sSup_smul_of_nonneg — Mathlib

English

For a ≥ 0, sSup(a · S) = a · sSup S.

Русский

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

LaTeX

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

Lean4

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

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