biSup_prod — Mathlib

English

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

Русский

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

LaTeX

$$$$ \iSup_{x \in s \timesˢ t} f x = \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 = ⨆ (a ∈ s) (b ∈ t), f (a, b) :=
  by
  simp_rw [iSup_prod, mem_prod, iSup_and]
  exact iSup_congr fun _ => iSup_comm

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