iInf_mul' — Mathlib

English

Let a ∈ ENat and f: ι → ENat with the mild hypothesis that if a = 0 then ι is nonempty. Then (inf_i f(i)) · a = inf_i (f(i) · a).

Русский

Пусть a ∈ ENat и f: ι → ENat, при условии, что если a = 0, то ι не пусто. Тогда (⨅ i, f(i)) · a = ⨅ i, f(i) · a.

LaTeX

$$$ (a = 0 \rightarrow ι \text{ не пустой }) \rightarrow \left( \inf_i f_i \right) \cdot a = \inf_i (f_i \cdot a) $$$

Lean4

/-- A version of `iInf_mul` with a slightly more general hypothesis. -/
theorem iInf_mul' (h₀ : a = 0 → Nonempty ι) : (⨅ i, f i) * a = ⨅ i, f i * a := by simp_rw [mul_comm, mul_iInf' h₀]

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