Theorems · Theorem · order theory

biInf_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

4 results in Mathlib

Foundations

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

Assumes

CompleteLattice