biSup_add_biSup_le — Mathlib

English

If s and t are nonempty, then (⨆ i ∈ s, f i) + (⨆ j ∈ t, g j) ≤ a whenever ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a.

Русский

Если множества s и t непустые, то (⨆ i∈s, f i) + (⨆ j∈t, g j) ≤ a при условии ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a.

LaTeX

$$$ \exists s \neq \emptyset, \exists t \neq \emptyset, \forall i \in s, \forall j \in t, f i + g j ≤ a \Rightarrow (\sup_{i \in s} f_i) + (\sup_{j \in t} g_j) ≤ a $$$

Lean4

theorem biSup_add_biSup_le {ι κ : Type*} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty) {f : ι → ℕ∞}
    {g : κ → ℕ∞} {a : ℕ∞} (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

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