iSup_add_le_add_iSup — Mathlib

English

The supremum of pointwise sums is at most the sum of the sups: sup_x (u(x)+v(x)) ≤ (sup_x u(x)) + (sup_x v(x)).

Русский

Supremum по x от (u(x)+v(x)) не превосходит суммы supremumов: sup_x (u(x)+v(x)) ≤ sup_x u(x) + sup_x v(x).

LaTeX

$$$ \sup_{x} (u(x) + v(x)) \le (\sup_{x} u(x)) + (\sup_{x} v(x)) $$$

Lean4

theorem iSup_add_le_add_iSup : ⨆ x, (u + v) x ≤ (⨆ x, u x) + ⨆ x, v x :=
  iSup_le fun i ↦ add_le_add (le_iSup u i) (le_iSup v i)

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