biSup_prod' — Mathlib

English

Let f : β → γ → α with s ⊆ β and t ⊆ γ. Then ⨆ x ∈ s ×ˢ t, f x.1 x.2 equals ⨆ (a ∈ s) (b ∈ t), f a b.

Русский

Пусть f : β → γ → α, s ⊆ β, t ⊆ γ. Тогда ⨆ x ∈ s ×ˢ t, f x.1 x.2 = ⨆ (a ∈ s) (b ∈ t), f a b.

LaTeX

$$$$ \iSup_{x \in s \timesˢ t} f x.1 x.2 = \iSup_{a \in s} \iSup_{b \in t} f a b $$$$

Lean4

theorem biSup_prod' {f : β → γ → α} {s : Set β} {t : Set γ} : ⨆ x ∈ s ×ˢ t, f x.1 x.2 = ⨆ (a ∈ s) (b ∈ t), f a b :=
  biSup_prod

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