pairwise_disjoint_on_Ioo_pred — Mathlib

English

If α is a linear pre-order with PredOrder, and f is antitone, then the intervals Ioo (f n) (f (pred n)) are pairwise disjoint.

Русский

Если α линейный предпорядок и f антитонична, то интервалы Ioo (f n) (f (pred n)) попарно не пересекаются.

LaTeX

$$PairwiseDisjoint( { Ioo (f n) (f (pred n)) } )$$

Lean4

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

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