English
Under mild conditions, the infimum of f and the infimum of g add componentwise: iInf f + iInf g = ⨅ a, f(a) + g(a).
Русский
При условии существования подходящих связей выполняется: iInf f + iInf g = ⨅ a, f(a) + g(a).
LaTeX
$$$ \mathrm{iInf}\ f + \mathrm{iInf}\ g = \inf_{a} (f(a) + g(a)) $$$
Lean4
theorem iInf_add_iInf (h : ∀ i j, ∃ k, f k + g k ≤ f i + g j) : iInf f + iInf g = ⨅ a, f a + g a :=
suffices ⨅ a, f a + g a ≤ iInf f + iInf g from
le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) (iInf_le _ _)) this
calc
⨅ a, f a + g a ≤ ⨅ (a) (a'), f a + g a' :=
le_iInf₂ fun a a' =>
let ⟨k, h⟩ := h a a';
iInf_le_of_le k h
_ = iInf f + iInf g := by simp_rw [iInf_add, add_iInf]
