pairwise_disjoint_on_Ioc_pred — Mathlib

English

For a monotone f, the union of Ico intervals over a subrange collapses to the corresponding Ioc interval across endpoints.

Русский

Для монотонной f объединение интервалов Ico свёртывается к соответствующему Ioc-интервалу на концах.

LaTeX

$$\displaystyle \bigcup_{i=m}^{n-1} Ico(f(i), f(succ(i))) = Ioc(f(m), f(n))$$

Lean4

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

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