Theorems · Theorem · order theory

Finpartition.card_bind

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α] {a : α}
  {P : Finpartition a} (Q : (i : α) → i ∈ P.parts → Finpartition i),
  (P.bind Q).parts.card = ∑ A ∈ P.parts.attach, (Q ↑A ⋯).parts.card

Defined in

Mathlib.Order.Partition.Finpartition

Cited by

1 results in Mathlib

Foundations

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

Assumes

LatticeOrderBotIsModularLatticeDecidableEq