iInf_mul — Mathlib

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 _) _

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