iInf_mul — Mathlib

English

Let ι be a nonempty index set, f: ι → ENat, and a ∈ ENat. Then (inf_i f(i)) · a = inf_i (f(i) · a).

Русский

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

LaTeX

$$$ (ι \neq \varnothing) \rightarrow (\inf_i f_i) \cdot a = \inf_i (f_i \cdot a) $$$

Lean4

theorem iInf_mul [Nonempty ι] : (⨅ i, f i) * a = ⨅ i, f i * a := by simp_rw [mul_comm, mul_iInf]

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