iSup_biUnion — Mathlib

English

For s: Finset γ, t: γ → Finset α, and f: α → β, the supremum over the biUnion equals the supremum over nested sups: ⨆ y ∈ s.biUnion t, f y = ⨆ (x ∈ s) (y ∈ t x), f y.

Русский

Для s: Finset γ, t: γ → Finset α и f: α → β верно: ⨆ y ∈ s.biUnion t, f y = ⨆ (x ∈ s) (y ∈ t x), f y.

LaTeX

$$$$\\displaystyle \\sup_{y \\in s\\;\\mathrm{biUnion}\\; t} f(y) = \\sup_{x \\in s} \\sup_{y \\in t(x)} f(y). $$$$

Lean4

theorem iSup_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → β) :
    ⨆ y ∈ s.biUnion t, f y = ⨆ (x ∈ s) (y ∈ t x), f y := by simp [@iSup_comm _ α, iSup_and]

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