iInf_mul_of_ne — Mathlib

English

(a ≠ 0) → (inf_i f(i)) · a = inf_i (f(i) · a).

Русский

(a ≠ 0) → (⨅ i, f(i)) · a = ⨅ i, f(i) · a.

LaTeX

$$$ (a \neq 0) \rightarrow \left( \inf_i f_i \right) \cdot a = \inf_i (f_i \cdot a) $$$

Lean4

/-- If `a ≠ 0`, then right multiplication by `a` maps infimum to infimum.
See also `ENat.iInf_mul` that assumes `[Nonempty ι]` but does not require `a ≠ 0`. -/
theorem iInf_mul_of_ne (ha₀ : a ≠ 0) : (⨅ i, f i) * a = ⨅ i, f i * a :=
  iInf_mul' <| by simp [ha₀]

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