English
Very general version for distributivity of multiplication over an infimum (swap of factors). If hinfty and h₀ hold, then (iInf f_i) · a = iInf (f_i · a).
Русский
Очень общая версия распределения умножения над инфинумом (перевёртывание множителей). При выполнении условий hinfty и h₀: (iInf_i f_i) · a = iInf_i (f_i · a).
LaTeX
$$$\\bigwedge_i f_i \\cdot a = \\bigwedge_i (f_i \\cdot a)$$$
Lean4
/-- Very general version for distributivity of multiplication over an infimum.
See `ENNReal.iInf_mul_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_mul` for the special case assuming `Nonempty ι`. -/
theorem iInf_mul' (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) :
(⨅ i, f i) * a = ⨅ i, f i * a := by simpa only [mul_comm a] using mul_iInf' hinfty h₀
