sup_product_left — Mathlib

English

Let s ⊆ β and t ⊆ γ be finite, and f: β × γ → α. Then the supremum over the product s × t equals the supremum over i ∈ s of the supremum over j ∈ t of f(i,j).

Русский

Пусть s ⊆ β и t ⊆ γ конечны, и f: β × γ → α. Тогда супремум по произведению s × t равен супремуму по i∈s от супремума по j∈t от f(i,j).

LaTeX

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

Lean4

/-- See also `Finset.product_biUnion`. -/
theorem sup_product_left (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f ⟨i, i'⟩ :=
  eq_of_forall_ge_iff fun a => by simp [@forall_swap _ γ]

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