English
Multiplying by a fixed ENat on the left distributes over iSup: a * ⨆ i, f i = ⨆ i, a * f i.
Русский
Умножение слева на фиксированное ENat распределяется над iSup: a * ⨆ i, f i = ⨆ i, a * f i.
LaTeX
$$$a * \bigl(\sup_i f(i)\bigr) = \sup_i (a * f(i))$$
Lean4
theorem mul_iSup (a : ℕ∞) (f : ι → ℕ∞) : a * ⨆ i, f i = ⨆ i, a * f i :=
by
refine (iSup_le fun i ↦ mul_le_mul' rfl.le <| le_iSup_iff.2 fun _ a ↦ a i).antisymm' <| le_iSup_iff.2 fun d h ↦ ?_
obtain rfl | hne := eq_or_ne a 0
· simp
obtain hι | hι := isEmpty_or_nonempty ι
· simp
cases d with
| top => simp
| coe
d =>
have hlt : ⨆ i, f i < ⊤ := by
rw [lt_top_iff_ne_top]
intro htop
obtain ⟨i, hi : d < f i⟩ := (iSup_eq_top ..).1 htop d (by simp)
exact (((h i).trans_lt hi).trans_le (ENat.self_le_mul_left _ hne)).false
obtain ⟨j, hj⟩ := exists_eq_iSup_of_lt_top hlt
rw [← hj]
apply h
