iSup_sup_eq — Mathlib

English

For any f,g : ι → α, the supremum of pointwise maxima equals the maximum of the suprema: sup_x (f x ⊔ g x) = (sup_x f x) ⊔ (sup_x g x).

Русский

Для любых f,g: ι → α верно, что супремум по x от max(f x, g x) равен max(супремум по f, супремум по g).

LaTeX

$$$ \\sup_{x} (f(x) \\vee g(x)) = (\\sup_{x} f(x)) \\vee (\\sup_{x} g(x)). $$$

Lean4

theorem iSup_sup_eq : ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x :=
  le_antisymm (iSup_le fun _ => sup_le_sup (le_iSup _ _) <| le_iSup _ _)
    (sup_le (iSup_mono fun _ => le_sup_left) <| iSup_mono fun _ => le_sup_right)

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