iInf₂_add — Mathlib

English

Two-dimensional index infimum with a fixed shift distributes: ⨅ (i) (j), f(i,j) + a = ⨅ (i) (j), f(i,j) + a.

Русский

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

LaTeX

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

Lean4

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

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