English
See general distributivity of multiplication over infimum with swapped factors under mild hypotheses.
Русский
См. общую версию распределения умножения над инфинумумом с перестановкой множителей при мягких гипотезах.
LaTeX
$$$(\\bigwedge_i f_i) \\cdot a = \\bigwedge_i (f_i \\cdot a)$$$
Lean4
/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.
See `ENNReal.iInf_mul'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`. -/
theorem iInf_mul_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : (⨅ i, f i) * a = ⨅ i, f i * a :=
iInf_mul' (by simp [ha]) (by simp [ha₀])
