sSup_add — Mathlib

English

If there exist i with p(i) and j with q(j), and for all i,j, f(i) + g(j) ≤ a, then (⨆ i, ⨆ _ : p i, f i) + (⨆ j, ⨆ _ : q j, g j) ≤ a.

Русский

Если существуют i, p(i) и j, q(j) такие, что для всех i,j выполняется f(i) + g(j) ≤ a, то сумма двух би-супремумов не превышает a.

LaTeX

$$$ \exists i \; p(i) \rightarrow \exists j \; q(j) \rightarrow \forall i,\forall j, (f(i) + g(j) ≤ a) \rightarrow (\bigvee_i \bigvee_{x} f(i) ) + (\bigvee_j \bigvee_{y} g(j)) ≤ a $$$

Lean4

theorem sSup_add (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a := by rw [sSup_eq_iSup, biSup_add hs]

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