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} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} (hf : Monotone f) (m n : α) : ⋃ i ∈ Set.Ico m n, Set.Ioc (f i) (f (Order.succ i)) = 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} [LinearOrder α] [SuccOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioc (f n) (f (Order.succ n)))

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} [LinearOrder α] [SuccOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ico (f n) (f (Order.succ n)))

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} [LinearOrder α] [SuccOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioo (f n) (f (Order.succ n)))

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} [LinearOrder α] [PredOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioc (f (Order.pred n)) (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} [LinearOrder α] [PredOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ico (f (Order.pred n)) (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} [LinearOrder α] [PredOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioo (f (Order.pred n)) (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} [LinearOrder α] [SuccOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioc (f (Order.succ n)) (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} [LinearOrder α] [SuccOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ico (f (Order.succ n)) (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} [LinearOrder α] [SuccOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioo (f (Order.succ n)) (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} [LinearOrder α] [PredOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioc (f n) (f (Order.pred n)))

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} [LinearOrder α] [PredOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ico (f n) (f (Order.pred n)))

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} [LinearOrder α] [PredOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : Pairwise (Function.onFun Disjoint fun (n : α) => Set.Ioo (f n) (f (Order.pred n)))

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.