iInf_add — Mathlib

English

For a family f, shifting by a fixed ENNReal a commutes with the infimum: iInf f + a = ⨅ i, f(i) + a.

Русский

При смещении на фиксированное ENNReal a инфимума сохраняется в виде iInf f + a = ⨅ i, f(i) + a.

LaTeX

$$$ \mathrm{iInf}\ f + a = \inf_i (f(i) + a) $$$

Lean4

theorem iInf_add : iInf f + a = ⨅ i, f i + a :=
  le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) <| le_rfl)
    (tsub_le_iff_right.1 <| le_iInf fun _ => tsub_le_iff_right.2 <| iInf_le _ _)

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