iInf_add_iInf_of_monotone — Mathlib

English

If f and g are monotone and directed appropriately, then iInf f + iInf g = ⨅ a, f(a) + g(a).

Русский

Если f и g монотонусны и направлены, то 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_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≥ ·)] {f g : ι → ℝ≥0∞} (hf : Monotone f)
    (hg : Monotone g) : iInf f + iInf g = ⨅ a, f a + g a :=
  iInf_add_iInf fun i j ↦ (exists_le_le i j).imp fun _k ⟨hi, hj⟩ ↦ by gcongr <;> apply_rules

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