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 biUnion_Ici_Ico_map_succ {α : Type u_1} {β : Type u_2} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} {a : α} (hf : ∀ i ∈ Set.Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Set.Ici a)) : ⋃ i ∈ Set.Ici a, Set.Ico (f i) (f (Order.succ i)) = Set.Ici (f a)

Union formula for Set.Ico (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_Ico_map_succ_eq_Ici for the specialization a = ⊥.

theorem biUnion_Ici_Ioc_map_succ {α : Type u_1} {β : Type u_2} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} {a : α} (hf : ∀ i ∈ Set.Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Set.Ici a)) : ⋃ i ∈ Set.Ici a, Set.Ioc (f i) (f (Order.succ i)) = Set.Ioi (f a)

Union formula for Set.Ioc (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_Ioc_map_succ_eq_Ioi for the specialization a = ⊥.

theorem iUnion_Ico_map_succ_eq_Ici {α : Type u_1} {β : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} (hf : ∀ (a : α), f ⊥ ≤ f a) (h2f : ¬BddAbove (Set.range f)) : ⋃ (a : α), Set.Ico (f a) (f (Order.succ a)) = Set.Ici (f ⊥)

Special case a = ⊥ of biUnion_Ici_Ico_map_succ.

theorem iUnion_Ioc_map_succ_eq_Ioi {α : Type u_1} {β : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} (hf : ∀ (a : α), f ⊥ ≤ f a) (h2f : ¬BddAbove (Set.range f)) : ⋃ (a : α), Set.Ioc (f a) (f (Order.succ a)) = Set.Ioi (f ⊥)

Special case a = ⊥ of biUnion_Ici_Ioc_map_succ.

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.