mathlib3 documentation

order.succ_pred.interval_succ

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove

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

source
theorem monotone.bUnion_Ico_Ioc_map_succ {α : Type u_1} {β : Type u_2} [linear_order α] [succ_order α] [is_succ_archimedean α] [linear_order β] {f : α → β} (hf : monotone f) (m n : α) :
(⋃ (i : α) (H : 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)

source
theorem monotone.pairwise_disjoint_on_Ioc_succ {α : Type u_1} {β : Type u_2} [linear_order α] [succ_order α] [preorder β] {f : α → β} (hf : monotone f) :
pairwise (disjoint on λ (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.

source
theorem monotone.pairwise_disjoint_on_Ico_succ {α : Type u_1} {β : Type u_2} [linear_order α] [succ_order α] [preorder β] {f : α → β} (hf : monotone f) :
pairwise (disjoint on λ (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.

source
theorem monotone.pairwise_disjoint_on_Ioo_succ {α : Type u_1} {β : Type u_2} [linear_order α] [succ_order α] [preorder β] {f : α → β} (hf : monotone f) :
pairwise (disjoint on λ (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.

source
theorem monotone.pairwise_disjoint_on_Ioc_pred {α : Type u_1} {β : Type u_2} [linear_order α] [pred_order α] [preorder β] {f : α → β} (hf : monotone f) :
pairwise (disjoint on λ (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.

source
theorem monotone.pairwise_disjoint_on_Ico_pred {α : Type u_1} {β : Type u_2} [linear_order α] [pred_order α] [preorder β] {f : α → β} (hf : monotone f) :
pairwise (disjoint on λ (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.

source
theorem monotone.pairwise_disjoint_on_Ioo_pred {α : Type u_1} {β : Type u_2} [linear_order α] [pred_order α] [preorder β] {f : α → β} (hf : monotone f) :
pairwise (disjoint on λ (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.

source
theorem antitone.pairwise_disjoint_on_Ioc_succ {α : Type u_1} {β : Type u_2} [linear_order α] [succ_order α] [preorder β] {f : α → β} (hf : antitone f) :
pairwise (disjoint on λ (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.

source
theorem antitone.pairwise_disjoint_on_Ico_succ {α : Type u_1} {β : Type u_2} [linear_order α] [succ_order α] [preorder β] {f : α → β} (hf : antitone f) :
pairwise (disjoint on λ (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.

source
theorem antitone.pairwise_disjoint_on_Ioo_succ {α : Type u_1} {β : Type u_2} [linear_order α] [succ_order α] [preorder β] {f : α → β} (hf : antitone f) :
pairwise (disjoint on λ (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.

source
theorem antitone.pairwise_disjoint_on_Ioc_pred {α : Type u_1} {β : Type u_2} [linear_order α] [pred_order α] [preorder β] {f : α → β} (hf : antitone f) :
pairwise (disjoint on λ (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.

source
theorem antitone.pairwise_disjoint_on_Ico_pred {α : Type u_1} {β : Type u_2} [linear_order α] [pred_order α] [preorder β] {f : α → β} (hf : antitone f) :
pairwise (disjoint on λ (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.

source
theorem antitone.pairwise_disjoint_on_Ioo_pred {α : Type u_1} {β : Type u_2} [linear_order α] [pred_order α] [preorder β] {f : α → β} (hf : antitone f) :
pairwise (disjoint on λ (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.