Theorems · Theorem · order theory

Finpartition.bind_parts

∀ {α : 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 = P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts

Defined in

Mathlib.Order.Partition.Finpartition

Cited by

2 results in Mathlib

Foundations

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

Assumes

LatticeOrderBotIsModularLatticeDecidableEq