pairwise_disjoint_on_Ico_pred — Mathlib

English

If α is a linear order with succ, and f is monotone, then the family {Ico (f i) (f (succ i))} is pairwise disjoint.

Русский

Если α линейно упорядочено с операцией succ и f монотонна, то множество {Ico (f i) (f (succ i))} попарно непересекаются.

LaTeX

$$PairwiseDisjoint( { Ico(f i) (f(succ i)) } )$$

Lean4

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ico (f Order.pred n) (f n)` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ico_pred [PredOrder α] [Preorder β] {f : α → β} (hf : Monotone f) :
    Pairwise (Disjoint on fun n => Ico (f (pred n)) (f n)) := by simpa using hf.dual.pairwise_disjoint_on_Ioc_succ

Похожие утверждения