pairwise_disjoint_on_Ioo_succ — Mathlib

English

If f is monotone, the intervals Ioc (f i) (f (succ i)) are pairwise disjoint as i varies.

Русский

Если f монотонна, интервалы Ioc (f i) (f (succ i)) попарно непересекаются по i.

LaTeX

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

Lean4

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioo (f n) (f (Order.succ n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioo_succ [SuccOrder α] [Preorder β] {f : α → β} (hf : Monotone f) :
    Pairwise (Disjoint on fun n => Ioo (f n) (f (succ n))) :=
  hf.pairwise_disjoint_on_Ico_succ.mono fun _ _ h => h.mono Ioo_subset_Ico_self Ioo_subset_Ico_self

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