iInf_div — Mathlib

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

/-- See `ENNReal.iInf_div'` for the general case, and `ENNReal.iInf_div_of_ne` for another special
case that assumes `a ≠ ∞` but does not require `Nonempty ι`. -/
theorem iInf_div [Nonempty ι] (hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) : (⨅ i, f i) / a = ⨅ i, f i / a :=
  iInf_div' hinfty fun _ ↦ ‹Nonempty ι›

Похожие утверждения