add_iInf₂ — Mathlib

English

For a two-argument family f(i,j), adding a constant a distributes over the two-argument infimum: a + ⨅ i j, f(i,j) = ⨅ i j, a + f(i,j).

Русский

Для двухаргументной семействной функции f(i,j) сумма с константой a распр. над двойным iInf: a + ⨅ i j, f(i,j) = ⨅ i j, a + f(i,j).

LaTeX

$$$ a + \inf_{i,j} f(i,j) = \inf_{i,j} (a + f(i,j)) $$$

Lean4

theorem add_iInf₂ {κ : ι → Sort*} (f : (i : ι) → κ i → ℝ≥0∞) : a + ⨅ (i) (j), f i j = ⨅ (i) (j), a + f i j := by
  simp [add_iInf]

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