biSup_add_biSup_le' — Mathlib

English

Let p,q be predicates with h: ∀ i, p(i) → ∀ j, q(j) → f(i) + g(j) ≤ a. Then (⨆ i, ⨆_{p(i)} f(i)) + ⨆ j, ⨆_{q(j)} g(j) ≤ a.

Русский

Пусть существуют предикаты p,q и условие h: ∀ i, p(i) → ∀ j, q(j) → f(i) + g(j) ≤ a. Тогда (⨆ i, ⨆_{p(i)} f(i)) + (⨆ j, ⨆_{q(j)} g(j)) ≤ a.

LaTeX

$$$\\text{Exists } i:\\; p(i) \\\\; \\Rightarrow \\\\; (\\sup_i \\sup_{p(i)} f_i) + (\\sup_j \\sup_{q(j)} g_j) \\le a$$$

Lean4

theorem biSup_add_biSup_le' {p : ι → Prop} {q : κ → Prop} (hp : ∃ i, p i) (hq : ∃ j, q j) {g : κ → ℝ≥0∞}
    (h : ∀ i, p i → ∀ j, q j → f i + g j ≤ a) : (⨆ i, ⨆ _ : p i, f i) + ⨆ j, ⨆ _ : q j, g j ≤ a :=
  by
  simp_rw [biSup_add' hp, add_biSup' hq]
  exact iSup₂_le fun i hi => iSup₂_le (h i hi)

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