pairwise_disjoint_on_Ioc_succ — Mathlib

English

If f is monotone, the union over i between m and n of Ioc (f i) (f (succ i)) equals Ioc (f m) (f n).

Русский

Если f монотонна, объединение по i от m до n интервалов Ioc (f i) (f (succ i)) равно Ioc (f m) (f n).

LaTeX

$$\displaystyle \bigcup_{i \in [m,n)} Ioc(f(i), f(\operatorname{succ} i)) = Ioc(f(m), f(n))$$

Lean4

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioc (f n) (f (Order.succ n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioc_succ [SuccOrder α] [Preorder β] {f : α → β} (hf : Monotone f) :
    Pairwise (Disjoint on fun n => Ioc (f n) (f (succ n))) :=
  (pairwise_disjoint_on _).2 fun _ _ hmn =>
    disjoint_iff_inf_le.mpr fun _ ⟨⟨_, h₁⟩, ⟨h₂, _⟩⟩ => h₂.not_ge <| h₁.trans <| hf <| succ_le_of_lt hmn

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