Theorems · Theorem · order theory

Fintype.exists_disjointed_le

∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → α),
  ∃ g ≤ f, Finset.univ.sup g = Finset.univ.sup f ∧ Pairwise (Function.onFun Disjoint g)

For any finite family of elements f : ι → α, we can find a pairwise-disjoint family g bounded above by f and having the same supremum. This is non-canonical, depending on an arbitrary choice of ordering of ι.

Defined in

Mathlib.Order.Disjointed

Cited by

1 results in Mathlib

Foundations

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

Assumes

GeneralizedBooleanAlgebraFintype