Theorems · Theorem · order theory
sup_Ioc_disjointed_of_monotone
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {ι : Type u_3} [inst_1 : LinearOrder ι]
[inst_2 : LocallyFiniteOrder ι] [inst_3 : OrderBot ι] {f : ι → α},
Monotone f → ∀ {m n : ι}, n ≤ m → (Finset.Ioc n m).sup (disjointed f) = f m \ f n- Defined in
- Mathlib.Order.Disjointed
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- LinearOrderstatement and proof · cited by 8,572
- Bot.botproof · cited by 4,720
- Monotonestatement and proof · cited by 1,397
- OrderBotstatement and proof · cited by 1,055
- LocallyFiniteOrderstatement and proof · cited by 658
- Order.succproof · cited by 633
- SuccOrderproof · cited by 574
- Finset.supstatement and proof · cited by 530
- IsMaxproof · cited by 372
- Finset.Iocstatement and proof · cited by 301
- GeneralizedBooleanAlgebrastatement and proof · cited by 204
Cited by1
Results whose statement or proof uses this declaration.
- biUnion_Ioc_disjointed_of_monotoneproof · cited by 1