pairwise_disjoint_on_Ico_succ — Mathlib

English

If f is monotone, the family of sets {Ico (f i) (f (succ i))} is pairwise disjoint as i ranges over α.

Русский

Если f монотонна, семейство множеств {Ico (f i) (f (succ i))} парно неверно пересекается по i.

LaTeX

$$PairwiseDisjoint( { Ico(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.Ico (f n) (f (Order.succ n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ico_succ [SuccOrder α] [Preorder β] {f : α → β} (hf : Monotone f) :
    Pairwise (Disjoint on fun n => Ico (f n) (f (succ n))) :=
  (pairwise_disjoint_on _).2 fun _ _ hmn =>
    disjoint_iff_inf_le.mpr fun _ ⟨⟨_, h₁⟩, ⟨h₂, _⟩⟩ => h₁.not_ge <| (hf <| succ_le_of_lt hmn).trans h₂

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