Monotone.pairwise_disjoint_on_Ico_pred
theorem Monotone.pairwise_disjoint_on_Ico_pred :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
Monotone f → Pairwise (Disjoint on fun n => Set.Ico (f (Order.pred n)) (f n))
The theorem states that if `α` is a linear order with a predecessor operation, `β` is any preorder, and `f` is a function from `α` to `β` that is monotone (i.e., preserves the order), then the left-closed right-open intervals generated by `f`, specifically `Set.Ico (f (Order.pred n)) (f n)` for each `n` in `α`, are pairwise disjoint. This means that for any two different elements `i` and `j` in `α`, the corresponding intervals do not overlap, or in other words, their intersection is the bottom element (`⊥`) of the order.
More concisely: If `α` is a lined order with a predecessor operation, `β` is any preorder, and `f : α → β` is a monotone function, then the left-closed right-open intervals `Set.Ico (f (Order.pred n)) (f n)` for all `n` in `α` are pairwise disjoint, i.e., their intersections equal the bottom element of the order.
|
Monotone.pairwise_disjoint_on_Ioc_pred
theorem Monotone.pairwise_disjoint_on_Ioc_pred :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
Monotone f → Pairwise (Disjoint on fun n => Set.Ioc (f (Order.pred n)) (f n))
The theorem states that if `α` is a type endowed with a linear order and a predecessor operation, `β` is a type endowed with a preorder, and `f` is a monotone function from `α` to `β`, then the left-open right-closed intervals `Set.Ioc (f (Order.pred n)) (f n)`, where `Order.pred n` is the predecessor of `n`, are pairwise disjoint. In other words, for any two distinct elements `n` and `m` of the type `α`, their corresponding intervals do not overlap. This property is significant in the context of order theory and set theory, where it can be applied to ensure the disjointness of a family of intervals generated by a monotone function.
More concisely: If `α` is a type with a linear order and a monotone function `f` to a preordered type `β`, then for any distinct `n` and `m` in `α`, the intervals `[f(pred n), f n)` and `[f(pred m), f m)` are disjoint in `β`.
|
Monotone.biUnion_Ico_Ioc_map_succ
theorem Monotone.biUnion_Ico_Ioc_map_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α]
[inst_3 : LinearOrder β] {f : α → β},
Monotone f → ∀ (m n : α), ⋃ i ∈ Set.Ico m n, Set.Ioc (f i) (f (Order.succ i)) = Set.Ioc (f m) (f n)
The theorem `Monotone.biUnion_Ico_Ioc_map_succ` states that if `α` is a type with a linear order and an archimedean succession order, while `β` is a type with a linear order, then for any monotone function `f` from `α` to `β` and any two elements `m` and `n` of `α`, the union of all intervals (which are left-open and right-closed) from `f i` to `f (succ i)`, where `i` ranges over all elements in the left-closed and right-open interval from `m` to `n`, is equal to the interval (which is left-open and right-closed) from `f m` to `f n`. Here, `succ i` denotes the successor of `i`, which is the least element greater than `i` if such an element exists, or `i` itself if `i` is maximal.
More concisely: For a monotone function `f` from a linearly ordered and archimedean type `α` to a linearly ordered type `β`, the union of all left-open, right-closed intervals `[f i, f (succ i))` from `i` in `α` between `m` and `n` equals the left-open, right-closed interval `(f m, f n)`.
|
Monotone.pairwise_disjoint_on_Ioo_pred
theorem Monotone.pairwise_disjoint_on_Ioo_pred :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
Monotone f → Pairwise (Disjoint on fun n => Set.Ioo (f (Order.pred n)) (f n))
This theorem states that given two types `α` and `β`, where `α` is a linear order with a predecessor operation and `β` is a preorder, if there exists a monotone function `f` from `α` to `β`, then the open intervals `Set.Ioo (f (Order.pred n)) (f n)` for all `n` in `α` are pairwise disjoint. In other words, for any two distinct elements `n` and `m` in `α`, the intervals `(f (Order.pred n), f n)` and `(f (Order.pred m), f m)` have no elements in common.
More concisely: Given a linear order `α` with a predecessor operation and a preorder `β`, if there exists a monotone function `f` from `α` to `β`, then for all distinct `n` and `m` in `α`, the open intervals `(f (Order.pred n), f n)` and `(f (Order.pred m), f m)` are disjoint in `β`.
|
Monotone.pairwise_disjoint_on_Ico_succ
theorem Monotone.pairwise_disjoint_on_Ico_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
Monotone f → Pairwise (Disjoint on fun n => Set.Ico (f n) (f (Order.succ n)))
This theorem states that if `α` is a type with a linear order and a successor function, and `β` is a type with a preorder, and if we have a monotone function `f` from `α` to `β`, then the intervals of the form `Set.Ico (f n) (f (Order.succ n))` are pairwise disjoint. In other words, for any two distinct elements `n` and `m` in `α`, the interval starting from `f n` and ending just before `f (Order.succ n)` does not overlap with the interval starting from `f m` and ending just before `f (Order.succ m)`. This is a property related to the order-preserving nature of the function `f` and the definition of the successor function in the linear order.
More concisely: If `f` is a monotonic function from a linearly ordered type `α` with successor function to a preordered type `β`, then for all distinct `n` and `m` in `α`, the intervals `[f n, f (Order.succ n))` and `[f m, f (Order.succ m))` are disjoint in `β`.
|
Antitone.pairwise_disjoint_on_Ioo_succ
theorem Antitone.pairwise_disjoint_on_Ioo_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
Antitone f → Pairwise (Disjoint on fun n => Set.Ioo (f (Order.succ n)) (f n))
The theorem `Antitone.pairwise_disjoint_on_Ioo_succ` states that for any two types `α` and `β`, where `α` is a linear order with a successor operation and `β` is a preorder, if we have an antitone function `f` from `α` to `β`, then the intervals `Set.Ioo (f (Order.succ n)) (f n)` are pairwise disjoint. Here, `Set.Ioo (f (Order.succ n)) (f n)` represents the open interval between `f (Order.succ n)` and `f n`, which contains all elements that are greater than `f (Order.succ n)` and less than `f n`. Pairwise disjoint means that any two different intervals do not have any common elements. In other words, the antitone function `f` ensures that the open intervals between the images of consecutive elements in the order `α` do not overlap.
More concisely: For any antitone function `f` from a linear order `α` with a successor operation to a preorder `β`, the open intervals `(f (suc n), f n)` in `β` are pairwise disjoint for all `n` in `α`.
|
Monotone.pairwise_disjoint_on_Ioc_succ
theorem Monotone.pairwise_disjoint_on_Ioc_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
Monotone f → Pairwise (Disjoint on fun n => Set.Ioc (f n) (f (Order.succ n)))
The theorem `Monotone.pairwise_disjoint_on_Ioc_succ` states that if `α` is a type with a linear order and a successor function, `β` is a type with a preorder, and `f : α → β` is a function that is monotone (meaning if `a ≤ b` then `f(a) ≤ f(b)`), then the intervals of the form `(f(n), f(succ(n))]` are pairwise disjoint. Here, `Set.Ioc (f n) (f (Order.succ n))` represents the interval from `f(n)` to `f(succ(n))`, excluding `f(n)` and including `f(succ(n))`, and `Disjoint on fun n => Set.Ioc (f n) (f (Order.succ n))` represents the property that these intervals do not overlap for different values of `n`. In other words, each `n` in `α` maps to a unique interval in `β` that does not overlap with the intervals corresponding to other values of `n`. Moreover, these intervals are ordered, reflecting the ordering in `α`.
More concisely: If `α` is a linearly ordered type with a successor function, `β` is a preordered type, and `f : α → β` is a monotone function, then the images of intervals of the form `(n, succ(n))` under `f` are pairwise disjoint.
|
Antitone.pairwise_disjoint_on_Ioc_pred
theorem Antitone.pairwise_disjoint_on_Ioc_pred :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
Antitone f → Pairwise (Disjoint on fun n => Set.Ioc (f n) (f (Order.pred n)))
The theorem `Antitone.pairwise_disjoint_on_Ioc_pred` states that if we have two types `α` and `β` where `α` has a linear order and a predecessor order, and `β` is a preorder, and we have an antitone function `f` from `α` to `β`, then the left-open right-closed intervals `Set.Ioc (f n) (f (Order.pred n))` are pairwise disjoint. In other words, for any two different elements `n` and `m` in `α`, their corresponding intervals from `f n` to `f (Order.pred n)` and from `f m` to `f (Order.pred m)` do not overlap in `β`. Here, `Order.pred n` refers to the greatest element less than `n` in `α`, if such an element exists; otherwise, it is `n` itself.
More concisely: For an antitone function `f` from a linearly ordered type `α` with a predecessor order to a preordered type `β`, the left-open right-closed intervals `Ioc (fn) (f (Order.pred n))` for distinct elements `n` in `α` are disjoint.
|
Antitone.pairwise_disjoint_on_Ico_pred
theorem Antitone.pairwise_disjoint_on_Ico_pred :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
Antitone f → Pairwise (Disjoint on fun n => Set.Ico (f n) (f (Order.pred n)))
The theorem states that for any antitone function `f` mapping from a linear pred order `α` to a preorder `β`, the left-closed right-open intervals formed by applying `f` to any element `n` and its predecessor `Order.pred n` are pairwise disjoint. This means that for any two distinct elements `i` and `j` in `α`, the intervals `Set.Ico (f i) (f (Order.pred i))` and `Set.Ico (f j) (f (Order.pred j))` do not overlap. In other words, no element in the preorder `β` belongs to more than one such interval.
More concisely: For any antitone function `f` from a linear preorder `α` to a preorder `β`, the intervals `Set.Ico (f (suc i)) (f i)` for distinct `i` in `α` are pairwise disjoint.
|
Antitone.pairwise_disjoint_on_Ioc_succ
theorem Antitone.pairwise_disjoint_on_Ioc_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
Antitone f → Pairwise (Disjoint on fun n => Set.Ioc (f (Order.succ n)) (f n))
The theorem `Antitone.pairwise_disjoint_on_Ioc_succ` states that for any linear order `α` with a successor function, any preorder `β`, and any antitone function `f` from `α` to `β`, the intervals `Set.Ioc (f (Order.succ n)) (f n)` (which are left-open right-closed intervals in the preorder `β` from `f` of the successor of `n` to `f` of `n`) are pairwise disjoint. Pairwise disjointness here means that any two different such intervals do not have any elements in common. This is a generalization of the idea that the successor of a number in a total ordering is always greater than the number itself, meaning ranges defined by a number and its successor should not overlap.
More concisely: For any linear order with successor function, any preorder, and any antitone function, the intervals defined by successive applications of the function on elements are pairwise disjoint.
|
Antitone.pairwise_disjoint_on_Ioo_pred
theorem Antitone.pairwise_disjoint_on_Ioo_pred :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
Antitone f → Pairwise (Disjoint on fun n => Set.Ioo (f n) (f (Order.pred n)))
The theorem `Antitone.pairwise_disjoint_on_Ioo_pred` claims that for any antitone function `f` from a type `α` to a type `β`, where `α` is a linear order with a pred function and `β` is a preorder, the left-open right-open intervals - defined as `Set.Ioo (f n) (f (Order.pred n))` where `n` is any element of `α` - are pairwise disjoint. Here, being antitone means that if `a ≤ b` then `f b ≤ f a`, pairwise disjoint means no two intervals share a common element, and the interval `Set.Ioo (f n) (f (Order.pred n))` is a set of elements `x` from the preorder `β` such that `f n < x < f (Order.pred n)`. The predecessor `Order.pred n` of an element `n` is the greatest element less than `n` if `n` is not minimal, otherwise it's `n` itself.
More concisely: For any antitone function from a linearly ordered type with pred function to a preorder, the left-open right-open intervals defined by the function are pairwise disjoint.
|
Monotone.pairwise_disjoint_on_Ioo_succ
theorem Monotone.pairwise_disjoint_on_Ioo_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
Monotone f → Pairwise (Disjoint on fun n => Set.Ioo (f n) (f (Order.succ n)))
The theorem `Monotone.pairwise_disjoint_on_Ioo_succ` states that if there exists a type `α` that is structured by a linear successor order, and another type `β` that is structured by a preorder, and if we have a monotone function `f : α → β`, then the intervals `Set.Ioo (f n) (f (Order.succ n))` are pairwise disjoint. In other words, for any two different elements `n` and `m` in `α`, the open interval between `f n` and `f (Order.succ n)` in `β` does not overlap with the open interval between `f m` and `f (Order.succ m)`. This means that the outputs of our function `f` don't overlap when considered within the intervals from any number to its successor order under `f`.
More concisely: For a monotone function `f` from a linearly ordered type `α` to a preordered type `β`, the images of non-overlapping open intervals under `f` are pairwise disjoint.
|
Antitone.pairwise_disjoint_on_Ico_succ
theorem Antitone.pairwise_disjoint_on_Ico_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
Antitone f → Pairwise (Disjoint on fun n => Set.Ico (f (Order.succ n)) (f n))
The theorem `Antitone.pairwise_disjoint_on_Ico_succ` states that for any given types `α` (with a linear order and a successor order) and `β` (with a preorder), and an antitone function `f` mapping from `α` to `β`, all intervals of the form `Set.Ico (f (Order.succ n)) (f n)` are pairwise disjoint. Here, pairwise disjoint means that the intersection of any two distinct intervals is empty, and an interval `Set.Ico a b` consists of all elements `x` such that `a ≤ x < b`. An antitone function is one that reverses the order: if `a ≤ b` then `f(b) ≤ f(a)`. The successor of an element `n` is the least element greater than `n` if such an element exists, otherwise it is `n` itself.
More concisely: For any antitone function `f` from a linearly ordered type `α` to a preordered type `β`, the intervals `Set.Ico (f (Order.succ n)) (f n)` are pairwise disjoint for all `n` in `α`.
|