English
For a function f and a, iInf f times a equals iInf of i ↦ f(i)·a.
Русский
Для функции f и элемента a справедливо iInf f · a = iInf_i (f(i)·a).
LaTeX
$$$\\\\forall {\\\\iota} (f : \\\\iota \\\\to \\\\mathbb{R}_{\\\\ge 0}) (a \\\\in \\\\mathbb{R}_{\\\\ge 0}), \\\\ iInf f * a = \\\\iInf i, f i * a.$$$
Lean4
theorem iInf_mul (f : ι → ℝ≥0) (a : ℝ≥0) : iInf f * a = ⨅ i, f i * a :=
by
rw [← coe_inj, NNReal.coe_mul, coe_iInf, coe_iInf]
exact Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _