English
If a ≠ 0 and a ≠ ∞, then right multiplication by a maps infimum to infimum: a · ⨅ i f_i = ⨅ i (a · f_i).
Русский
Если a ≠ 0 и a ≠ ∞, то умножение справа на a отображает инфиминум в инфиминум: a · ⨅ i f_i = ⨅ i (a · f_i).
LaTeX
$$$a \\neq 0 \\;\\land\\; a \\neq \\infty \\;\\Rightarrow\\; a \\cdot \\big(\\bigwedge_i f_i\\big) = \\bigwedge_i (a \\cdot f_i)$$$
Lean4
/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.
See `ENNReal.mul_iInf'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`, and `ENNReal`. -/
theorem mul_iInf_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * ⨅ i, f i = ⨅ i, a * f i :=
mul_iInf' (by simp [ha]) (by simp [ha₀])
