mul_iInf_of_ne — Mathlib

English

If a ≠ 0, then right multiplication by a preserves the infimum: a · (inf_i f(i)) = inf_i (a · f(i)).

Русский

Если a ≠ 0, то умножение справа на a сохраняет инфимума: a · (⨅ i, f(i)) = ⨅ i, a · f(i).

LaTeX

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

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 mul_iInf_of_ne (ha₀ : a ≠ 0) : a * ⨅ i, f i = ⨅ i, a * f i :=
  mul_iInf' <| by simp [ha₀]

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