# Documentation

Mathlib.Order.SuccPred.IntervalSucc

# Intervals Ixx (f x) (f (Order.succ x))#

In this file we prove

• Monotone.biUnion_Ico_Ioc_map_succ: if α is a linear archimedean succ order and β is a linear order, then for any monotone function f and m n : α, the union of intervals Set.Ioc (f i) (f (Order.succ i)), m ≤ i < n, is equal to Set.Ioc (f m) (f n);

• Monotone.pairwise_disjoint_on_Ioc_succ: 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.

For the latter lemma, we also prove various order dual versions.

theorem Monotone.biUnion_Ico_Ioc_map_succ {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) (m : α) (n : α) :
⋃ (i : α) (_ : i Set.Ico m n), Set.Ioc (f i) (f ()) = Set.Ioc (f m) (f n)

If α is a linear archimedean succ order and β is a linear order, then for any monotone function f and m n : α, the union of intervals Set.Ioc (f i) (f (Order.succ i)), m ≤ i < n, is equal to Set.Ioc (f m) (f n)

theorem Monotone.pairwise_disjoint_on_Ioc_succ {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioc (f n) (f ()))

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 Monotone.pairwise_disjoint_on_Ico_succ {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ico (f n) (f ()))

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 Monotone.pairwise_disjoint_on_Ioo_succ {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioo (f n) (f ()))

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 Monotone.pairwise_disjoint_on_Ioc_pred {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioc (f ()) (f n))

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 Monotone.pairwise_disjoint_on_Ico_pred {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ico (f ()) (f n))

If α is a linear pred order, β is a preorder, and f : α → β is a monotone function, then the intervals Set.Ico (f Order.pred n) (f n) are pairwise disjoint.

theorem Monotone.pairwise_disjoint_on_Ioo_pred {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioo (f ()) (f n))

If α is a linear pred order, β is a preorder, and f : α → β is a monotone function, then the intervals Set.Ioo (f Order.pred n) (f n) are pairwise disjoint.

theorem Antitone.pairwise_disjoint_on_Ioc_succ {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioc (f ()) (f n))

If α is a linear succ order, β is a preorder, and f : α → β is an antitone function, then the intervals Set.Ioc (f (Order.succ n)) (f n) are pairwise disjoint.

theorem Antitone.pairwise_disjoint_on_Ico_succ {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ico (f ()) (f n))

If α is a linear succ order, β is a preorder, and f : α → β is an antitone function, then the intervals Set.Ico (f (Order.succ n)) (f n) are pairwise disjoint.

theorem Antitone.pairwise_disjoint_on_Ioo_succ {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioo (f ()) (f n))

If α is a linear succ order, β is a preorder, and f : α → β is an antitone function, then the intervals Set.Ioo (f (Order.succ n)) (f n) are pairwise disjoint.

theorem Antitone.pairwise_disjoint_on_Ioc_pred {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioc (f n) (f ()))

If α is a linear pred order, β is a preorder, and f : α → β is an antitone function, then the intervals Set.Ioc (f n) (f (Order.pred n)) are pairwise disjoint.

theorem Antitone.pairwise_disjoint_on_Ico_pred {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ico (f n) (f ()))

If α is a linear pred order, β is a preorder, and f : α → β is an antitone function, then the intervals Set.Ico (f n) (f (Order.pred n)) are pairwise disjoint.

theorem Antitone.pairwise_disjoint_on_Ioo_pred {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
Pairwise (Disjoint on fun n => Set.Ioo (f n) (f ()))

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.