Theorems · Theorem · order theory

Finpartition.mem_bind

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {a b : α} {P : Finpartition a} {Q : (i : α) → i ∈ P.parts → Finpartition i},
  b ∈ (P.bind Q).parts ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Defined in

Mathlib.Order.Partition.Finpartition

Cited by

1 results in Mathlib

Foundations

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

Assumes

LatticeOrderBotIsModularLatticeDecidableEq