Theorems · Theorem · order theory

biInf_sup_biInf

∀ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : Set ι}
  {t : Set ι'}, (⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j = ⨅ p ∈ s ×ˢ t, f p.1 ⊔ g p.2

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

2 results in Mathlib

Foundations

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

Assumes

Order.Coframe