Theorems · Theorem · order theory

biSup_inter_of_pairwise_disjoint

∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {f : ι → α},
  Pairwise (Function.onFun Disjoint f) → ∀ (s t : Set ι), ⨆ i ∈ s ∩ t, f i = (⨆ i ∈ s, f i) ⊓ ⨆ i ∈ t, f i

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Order.Frame