English
For NNReal sequences and a, if for all i there is a bound a ≤ f(i) then a ≤ inf_i f(i) + inf_j g(j).
Русский
Для NNReal-последовательностей и a, если ∀ i,j: a ≤ f(i) + g(j), то a ≤ inf_i f(i) + inf_j g(j).
LaTeX
$$$\\\\forall {\\\\iota} {\\\\iota'}, \\\\ [Nonempty \\\\iota] [Nonempty \\\\iota'] \\\\ {f : \\\\iota \\\\to \\\\mathbb{R}_{\\\\ge 0}} {g : \\\\iota' \\\\to \\\\mathbb{R}_{\\\\ge 0}} {a : \\\\mathbb{R}_{\\\\ge 0}} \\\\left( \\\\forall i j, a \\\\le f i + g j \\right) \\\\Rightarrow a \\\\le (\\\\inf i, f i) + \\\\inf j, g j.$$$
Lean4
theorem le_iInf_add_iInf {ι ι' : Sort*} [Nonempty ι] [Nonempty ι'] {f : ι → ℝ≥0} {g : ι' → ℝ≥0} {a : ℝ≥0}
(h : ∀ i j, a ≤ f i + g j) : a ≤ (⨅ i, f i) + ⨅ j, g j :=
by
rw [← NNReal.coe_le_coe, NNReal.coe_add, coe_iInf, coe_iInf]
exact le_ciInf_add_ciInf h
