biSup_add_biSup_le — Mathlib

English

Let s,t be nonempty sets of indices and f,g arbitrary with h: ∀ i ∈ s, ∀ j ∈ t, f(i) + g(j) ≤ a. Then (sup_{i∈s} f_i) + (sup_{j∈t} g_j) ≤ a.

Русский

Пусть s,t непусты, и для всех i∈s, j∈t выполняется f(i) + g(j) ≤ a. Тогда (sup_{i∈s} f_i) + (sup_{j∈t} g_j) ≤ a.

LaTeX

$$$\\sup_{i\\in s} f_i + \\sup_{j\\in t} g_j \\le a$$$

Lean4

theorem biSup_add_biSup_le {ι κ : Type*} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty) {f : ι → ℝ≥0∞}
    {g : κ → ℝ≥0∞} {a : ℝ≥0∞} (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) : (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a :=
  biSup_add_biSup_le' hs ht h

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