English
Let a ∈ ENat and f: ι → ENat with the mild hypothesis that if a = 0 then ι is nonempty. Then a · (inf_i f(i)) = inf_i (a · f(i)).
Русский
Пусть a ∈ ENat и f: ι → ENat, с условием: если a = 0, то ι непусто. Тогда a · (⨅ i, f(i)) = ⨅ i, a · f(i).
LaTeX
$$$ (a = 0 \rightarrow ι \text{ не пустой }) \rightarrow a \cdot \inf_i f_i = \inf_i (a \cdot f_i) $$$
Lean4
/-- A version of `mul_iInf` with a slightly more general hypothesis. -/
theorem mul_iInf' (h₀ : a = 0 → Nonempty ι) : a * ⨅ i, f i = ⨅ i, a * f i :=
by
obtain hι | hι := isEmpty_or_nonempty ι
· suffices a ≠ 0 by simpa [iInf_of_empty, ite_eq_right_iff, mul_top']
aesop
rw [mul_iInf]
