Theorems · Definition · order theory

Finpartition.extend

{α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      [IsModularLattice α] →
        [DecidableEq α] → {a b c : α} → Finpartition a → b ≠ ⊥ → Disjoint a b → a ⊔ b = c → Finpartition c

Adds b to a finpartition of a to make a finpartition of a ⊔ b.

Defined in

Mathlib.Order.Partition.Finpartition

Cited by

5 results in Mathlib

Foundations

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

Assumes

LatticeOrderBotIsModularLatticeDecidableEq