Theorems · Theorem · order theory

Monotone.disjointed_succ_sup

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

Note this lemma does not require ¬IsMax i, unlike disjointed_succ.

Defined in

Mathlib.Order.Disjointed

Cited by

1 results in Mathlib

Foundations

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

Assumes

GeneralizedBooleanAlgebraLinearOrderLocallyFiniteOrderBotSuccOrder