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