mul_iInf — Mathlib

English

If ι is nonempty, right multiplication by a maps infimum to infimum: (iInf_i f_i) · a = iInf_i (f_i · a).

Русский

Если множество индексов непусто, то умножение справа на a сохраняет инфиминум: (iInf_i f_i) · a = iInf_i (f_i · a).

LaTeX

$$$\\bigwedge_i f_i \\cdot a = \\bigwedge_i (f_i \\cdot a)$$$

Lean4

/-- See `ENNReal.mul_iInf'` for the general case, and `ENNReal.mul_iInf_of_ne` for another special
case that assumes `a ≠ 0` but does not require `Nonempty ι`. -/
theorem mul_iInf [Nonempty ι] (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) : a * ⨅ i, f i = ⨅ i, a * f i :=
  mul_iInf' hinfty fun _ ↦ ‹Nonempty ι›

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