sSup_image2 — Mathlib

English

Let f: β → γ → α, s ⊆ β, t ⊆ γ. Then the supremum of the image2 f on s × t equals the iterated supremum over a ∈ s and b ∈ t of f a b.

Русский

Пусть f: β → γ → α, s ⊆ β, t ⊆ γ. Тогда верхняя грань образа image2 f над s×t равна поочередному верхнему пределу по a ∈ s и b ∈ t: sSup(image2 f s t) = ∑_{a∈s} ∑_{b∈t} f(a,b).

LaTeX

$$$sSup(\\mathrm{image2}\\,f\\,s\\,t) = \\big\\vee_{a \\in s} \\big\\vee_{b \\in t} f(a,b)$$$

Lean4

theorem sSup_image2 {f : β → γ → α} {s : Set β} {t : Set γ} : sSup (image2 f s t) = ⨆ (a ∈ s) (b ∈ t), f a b := by
  rw [← image_prod, sSup_image, biSup_prod]

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