le_iInf₂_add_iInf₂ — Mathlib

English

A higher-dimensional version: if a ≤ f(i,pi) + g(k,qk) for all i,pi,k,qk, then a ≤ iInf over i,pi and k,qk of f(i,pi) plus iInf over k,qk of g(k,qk).

Русский

В более общем виде: если а ≤ f(i,π) + g(k,𝒬) для всех аргументов, то a ≤ iInf f + iInf g.

LaTeX

$$$ a \le (iInf f) + (iInf g) \quad\text{under appropriate indexing}$$$

Lean4

theorem le_iInf₂_add_iInf₂ {q₁ : ι → Sort*} {q₂ : κ → Sort*} {f : (i : ι) → q₁ i → ℝ≥0∞} {g : (k : κ) → q₂ k → ℝ≥0∞}
    (h : ∀ i pi k qk, a ≤ f i pi + g k qk) : a ≤ (⨅ (i) (qi), f i qi) + ⨅ (k) (qk), g k qk :=
  by
  simp_rw [iInf₂_add, add_iInf₂]
  exact le_iInf₂ fun i hi => le_iInf₂ (h i hi)

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