pairwise_disjoint_on_Ioo_pred — Mathlib

English

If α is linear succ order and f is antitone, the Ioc (f(n+1)) (f n) intervals are pairwise disjoint.

Русский

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

LaTeX

$$PairwiseDisjoint( { Ioc (f (succ n)) (f n) } )$$

Lean4

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

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