mul_iInf — Mathlib

English

Multiplication distributes over iInf: a · iInf f = iInf (i ↦ a · f i).

Русский

Умножение распределяется по iInf: a · iInf f = iInf (i ↦ a · f i).

LaTeX

$$$\\\\forall {\\\\iota} (f : \\\\iota \\\\to \\\\mathbb{R}_{\\\\ge 0}) (a \\\\in \\\\mathbb{R}_{\\\\ge 0}), \\\\ a * iInf f = iInf (\\\\lambda i. a * f i).$$$

Lean4

theorem mul_iInf (f : ι → ℝ≥0) (a : ℝ≥0) : a * iInf f = ⨅ i, a * f i := by simpa only [mul_comm] using iInf_mul f a

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