Theorems · Definition · order theory

Finpartition.combine

{α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      [IsModularLattice α] →
        [DecidableEq α] →
          {ι : Type u_2} →
            {I : Finset ι} → {a : ι → α} → ((i : ι) → Finpartition (a i)) → I.SupIndep a → Finpartition (I.sup a)

Combine a family of partitions of pairwise disjoint elements into a partition of their sup.

Defined in

Mathlib.Order.Partition.Finpartition

Cited by

4 results in Mathlib

Foundations

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

Assumes

LatticeOrderBotIsModularLatticeDecidableEq