Theorems · Theorem · order theory

Finpartition.card_extend

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α] {a : α}
  (P : Finpartition a) (b c : α) {hb : b ≠ ⊥} {hab : Disjoint a b} {hc : a ⊔ b = c},
  (P.extend hb hab hc).parts.card = P.parts.card + 1

Defined in

Mathlib.Order.Partition.Finpartition

Cited by

0 results in Mathlib

Foundations

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

Assumes

LatticeOrderBotIsModularLatticeDecidableEq