Theorems · Theorem · order theory

Finpartition.mem_parts_or_eq_sdiff_of_mem_extendOfLE

∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hab : a ≤ b) {p : α}, p ∈ (P.extendOfLE hab).parts → p ∈ P.parts ∨ p = b \ a

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

GeneralizedBooleanAlgebraDecidableEq