iInf_mul — Mathlib

English

See generalized distributivity of multiplication over infimum (alternative formulation).

Русский

См. обобщённая форма распределения умножения над инфинумумом (альтернативная постановка).

LaTeX

$$$\\bigwedge_i f_i \\cdot a = \\bigwedge_i (f_i \\cdot a)$$$

Lean4

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

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