English
Very general version for distributivity of multiplication over an infimum. If hinfty and h₀ hold, then a * ⨅ i, f i = ⨅ i, a * f i.
Русский
Очень общая версия распределения умножения над инфиминумом. При выполнении условий hinfty и h₀ имеет место: a · ⨅ i f(i) = ⨅ i (a · f(i)).
LaTeX
$$$a \\cdot \\big(\\bigwedge_i f_i\\big) = \\bigwedge_i a \\cdot f_i$$$
Lean4
/-- Very general version for distributivity of multiplication over an infimum.
See `ENNReal.mul_iInf_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.mul_iInf` for the special case assuming `Nonempty ι`. -/
theorem mul_iInf' (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) :
a * ⨅ i, f i = ⨅ i, a * f i := by
obtain rfl | ha₀ := eq_or_ne a 0
· simp [h₀ rfl]
obtain rfl | ha := eq_or_ne a ∞
· obtain ⟨i, hi⟩ | hf := em (∃ i, f i = 0)
· rw [(iInf_eq_bot _).2, (iInf_eq_bot _).2, bot_eq_zero, mul_zero] <;> exact fun _ _ ↦ ⟨i, by simpa [hi]⟩
· rw [top_mul (mt (hinfty rfl) hf), eq_comm, iInf_eq_top]
exact fun i ↦ top_mul fun hi ↦ hf ⟨i, hi⟩
· exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iInf _
