Theorems · Theorem · order theory

Finpartition.combine_parts

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {ι : Type u_2} {I : Finset ι} {a : ι → α} (P : (i : ι) → Finpartition (a i)) (ha : I.SupIndep a),
  (Finpartition.combine P ha).parts = I.biUnion fun i => (P i).parts

Defined in: Mathlib.Order.Partition.Finpartition
Cited by: 0 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Lattice OrderBot IsModularLattice DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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
OrderBotstatement and proof · cited by 1,055
Latticestatement and proof · cited by 916
Finset.supstatement · cited by 530
Finset.biUnionstatement · cited by 217
Finpartitionstatement and proof · cited by 199
Finpartition.partsstatement and proof · cited by 184
IsModularLatticestatement and proof · cited by 86
Finset.SupIndepstatement and proof · cited by 52
Finpartition.combinestatement and proof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.