mul_iInf — Mathlib

English

Multiplication by a fixed ENat on the left distributes over iInf: a * ⨅ i, f i = ⨅ i, a * f i.

Русский

Умножение слева на фиксированное ENat распределяется над iInf: a * ⨅ i, f i = ⨅ i, a * f i.

LaTeX

$$$a * \inf_i f(i) = \inf_i (a * f(i))$$$

Lean4

theorem mul_iInf [Nonempty ι] : a * ⨅ i, f i = ⨅ i, a * f i :=
  by
  refine (le_iInf fun x ↦ (mul_le_mul_left' (iInf_le ..) a)).antisymm ?_
  obtain ⟨b, hb⟩ := ENat.exists_eq_iInf f
  rw [← hb, iInf_le_iff]
  exact fun x h ↦ h _

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