iSup_union — Mathlib

English

For Finset α, Finset β, and f: α → β, the supremum over the union equals the supremum of the two sups: ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ (⨆ x ∈ t, f x).

Русский

Для Finset α, Finset β и функции f верно: ⨆ x ∈ s ∪ t, f x = ⨆ x ∈ s, f x ⊔ ⨆ x ∈ t, f x.

LaTeX

$$$$\\displaystyle \\sup_{x \\in s \\cup t} f(x) = \\max\\left( \\sup_{x \\in s} f(x), \\sup_{x \\in t} f(x) \\right). $$$$

Lean4

theorem iSup_union {f : α → β} {s t : Finset α} : ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x := by
  simp [iSup_or, iSup_sup_eq]

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