iSup_union — Mathlib

English

For any f: β → α and subsets s, t ⊆ β, the supremum over s ∪ t equals the join of the sups over s and t: ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ (⨆ x ∈ t, f x).

Русский

Для любых f: β → α и подмножеств s, t ⊆ β супремум по s ∪ t равен объединению двух су́п по s и по t.

LaTeX

$$$$ \\sup_{x \\in s \\cup t} f(x) = \\bigl( \\sup_{x \\in s} f(x) \\bigr) \\vee \\bigl( \\sup_{x \\in t} f(x) \\bigr) $$$$

Lean4

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

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