sup_product_right — Mathlib

English

Dual of Sup Product Left: the supremum over the product s × t equals the supremum over i' ∈ t of the supremum over i ∈ s of f(i,i').

Русский

Двойственность к Sup Product Left: супремум по произведению равен супремуму по i' из t от супремума по i из s от f(i,i').

LaTeX

$$$ (s \\times^{\\mathrm{ˢ}} t).sup f = t.sup (\\lambda i'. s.sup (\\lambda i. f(i,i'))) $$$

Lean4

theorem sup_product_right (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f ⟨i, i'⟩ := by rw [sup_product_left, Finset.sup_comm]

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