Theorems · Definition · order theory

Finpartition.ofPairwiseDisjoint

{α : Type u_1} →
  [inst : DistribLattice α] →
    [inst_1 : OrderBot α] →
      [DecidableEq α] → (parts : Finset α) → (↑parts).PairwiseDisjoint id → Finpartition (parts.sup id)

A Finpartition constructor of parts.sup id from a finset parts of pairwise disjoint elements. Any ⊥ elements in parts are erased.

Defined in: Mathlib.Order.Partition.Finpartition
Cited by: 4 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DistribLattice OrderBot DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement and proof · cited by 13,712
SetLike.coestatement and proof · cited by 8,199
Bot.botproof · cited by 4,720
OrderBotstatement and proof · cited by 1,055
Finset.supstatement · cited by 530
Finset.eraseproof · cited by 455
Set.PairwiseDisjointstatement and proof · cited by 275
Finpartitionstatement · cited by 199
DistribLatticestatement and proof · cited by 150

Cited by4

Results whose statement or proof uses this declaration.

Finpartition.ofPairwiseDisjoint_partsstatement and proof · cited by 2
Finpartition.sum_ofPairwiseDisjoint_eq_sumstatement · cited by 1
MeasureTheory.VectorMeasure.le_variationproof · cited by 1
Finpartition.ofPairwiseDisjoint.congr_simpstatement and proof · cited by 0