Theorems · Theorem · order theory

biSup_prod

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ},
  ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

5 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

CompleteLattice