Theorems · Theorem · order theory

Antitone.pairwise_disjoint_on_Ioc_pred

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioc (f n) (f (Order.pred n)))

If α is a linear pred order, β is a preorder, and f : α → β is an antitone function, then the intervals Set.Ioc (f n) (f (Order.pred n)) are pairwise disjoint.

Defined in

Mathlib.Order.SuccPred.IntervalSucc

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderPredOrderPreorder