English
Let a ∈ ENNReal and f : I → ENNReal. Then a · (sup_i f(i)) = sup_i (a · f(i)).
Русский
Пусть a ∈ ENNReal и f : I → ENNReal. Тогда a умножение на $\sup_i f(i)$ равно $\sup_i (a · f(i))$.
LaTeX
$$$a \\cdot \\sup_i f_i = \\sup_i (a \\cdot f_i)$$$
Lean4
theorem mul_iSup (a : ℝ≥0∞) (f : ι → ℝ≥0∞) : a * ⨆ i, f i = ⨆ i, a * f i :=
by
by_cases hf : ∀ i, f i = 0
· simp [hf]
obtain rfl | ha₀ := eq_or_ne a 0
· simp
obtain rfl | ha := eq_or_ne a ∞
· obtain ⟨i, hi⟩ := not_forall.1 hf
simpa [iSup_eq_zero.not.2 hf, eq_comm (a := ⊤)] using le_iSup_of_le (f := fun i => ⊤ * f i) i (top_mul hi).ge
· exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _
