English
Very general version for division over an infimum; divides by a on both sides under mild hypotheses.
Русский
Очень общая версия деления над инфиминумом; по аналогии разделение на a сохраняет инфиминум при условии.
LaTeX
$$$(\\bigwedge_i f_i) / a = \\bigwedge_i (f_i / a)$$$
Lean4
/-- Very general version for distributivity of division over an infimum.
See `ENNReal.iInf_div_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_div` for the special case assuming `Nonempty ι`. -/
theorem iInf_div' (hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = ∞ → Nonempty ι) :
(⨅ i, f i) / a = ⨅ i, f i / a :=
iInf_mul' (by simpa) (by simpa)
