Theorems · Theorem · order theory

disjointed_succ

∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : SuccOrder ι] (f : ι → α) {i : ι},
  ¬IsMax i → disjointed f (Order.succ i) = f (Order.succ i) \ (partialSups f) i

Defined in

Mathlib.Order.Disjointed

Cited by

3 results in Mathlib

Foundations

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

Assumes

GeneralizedBooleanAlgebraLinearOrderLocallyFiniteOrderBotSuccOrder