About Quotient Orders and Ordering Sequences

Sebastian Koch. "About Quotient Orders and Ordering Sequences." Formalized Mathematics 25.2 (2017): 121-139. <http://eudml.org/doc/288462>.

@article{SebastianKoch2017,
abstract = {In preparation for the formalization in Mizar [4] of lotteries as given in [14], this article closes some gaps in the Mizar Mathematical Library (MML) regarding relational structures. The quotient order is introduced by the equivalence relation identifying two elements x, y of a preorder as equivalent if x ⩽ y and y ⩽ x. This concept is known (see e.g. chapter 5 of [19]) and was first introduced into the MML in [13] and that work is incorporated here. Furthermore given a set A, partition D of A and a finite-support function f : A → ℝ, a function Σf : D → ℝ, Σf (X)= ∑x∈X f(x) can be defined as some kind of natural “restriction” from f to D. The first main result of this article can then be formulated as: ∑x∈Af(x)=∑X∈DΣf(X)(=∑X∈D∑x∈Xf(x)) \[\sum \limits \_\{x \in A\} \{f(x)\} = \sum \limits \_\{X \in D\} \{\Sigma \_f (X)\left( \{ = \sum \limits \_\{X \in D\} \{\sum \limits \_\{x \in X\} \{f(x)\} \} \} \right)\} \] After that (weakly) ascending/descending finite sequences (based on [3]) are introduced, in analogous notation to their infinite counterparts introduced in [18] and [13]. The second main result is that any finite subset of any transitive connected relational structure can be sorted as a ascending or descending finite sequence, thus generalizing the results from [16], where finite sequence of real numbers were sorted. The third main result of the article is that any weakly ascending/weakly descending finite sequence on elements of a preorder induces a weakly ascending/weakly descending finite sequence on the projection of these elements into the quotient order. Furthermore, weakly ascending finite sequences can be interpreted as directed walks in a directed graph, when the set of edges is described by ordered pairs of vertices, which is quite common (see e.g. [10]). Additionally, some auxiliary theorems are provided, e.g. two schemes to find the smallest or the largest element in a finite subset of a connected transitive relational structure with a given property and a lemma I found rather useful: Given two finite one-to-one sequences s, t on a set X, such that rng t ⊆ rng s, and a function f : X → ℝ such that f is zero for every x ∈ rng s rng t, we have ∑ f o s = ∑ f o t.},
author = {Sebastian Koch},
journal = {Formalized Mathematics},
keywords = {quotient order; ordered finite sequences},
language = {eng},
number = {2},
pages = {121-139},
title = {About Quotient Orders and Ordering Sequences},
url = {http://eudml.org/doc/288462},
volume = {25},
year = {2017},
}

TY - JOUR
AU - Sebastian Koch
TI - About Quotient Orders and Ordering Sequences
JO - Formalized Mathematics
PY - 2017
VL - 25
IS - 2
SP - 121
EP - 139
AB - In preparation for the formalization in Mizar [4] of lotteries as given in [14], this article closes some gaps in the Mizar Mathematical Library (MML) regarding relational structures. The quotient order is introduced by the equivalence relation identifying two elements x, y of a preorder as equivalent if x ⩽ y and y ⩽ x. This concept is known (see e.g. chapter 5 of [19]) and was first introduced into the MML in [13] and that work is incorporated here. Furthermore given a set A, partition D of A and a finite-support function f : A → ℝ, a function Σf : D → ℝ, Σf (X)= ∑x∈X f(x) can be defined as some kind of natural “restriction” from f to D. The first main result of this article can then be formulated as: ∑x∈Af(x)=∑X∈DΣf(X)(=∑X∈D∑x∈Xf(x)) \[\sum \limits _{x \in A} {f(x)} = \sum \limits _{X \in D} {\Sigma _f (X)\left( { = \sum \limits _{X \in D} {\sum \limits _{x \in X} {f(x)} } } \right)} \] After that (weakly) ascending/descending finite sequences (based on [3]) are introduced, in analogous notation to their infinite counterparts introduced in [18] and [13]. The second main result is that any finite subset of any transitive connected relational structure can be sorted as a ascending or descending finite sequence, thus generalizing the results from [16], where finite sequence of real numbers were sorted. The third main result of the article is that any weakly ascending/weakly descending finite sequence on elements of a preorder induces a weakly ascending/weakly descending finite sequence on the projection of these elements into the quotient order. Furthermore, weakly ascending finite sequences can be interpreted as directed walks in a directed graph, when the set of edges is described by ordered pairs of vertices, which is quite common (see e.g. [10]). Additionally, some auxiliary theorems are provided, e.g. two schemes to find the smallest or the largest element in a finite subset of a connected transitive relational structure with a given property and a lemma I found rather useful: Given two finite one-to-one sequences s, t on a set X, such that rng t ⊆ rng s, and a function f : X → ℝ such that f is zero for every x ∈ rng s rng t, we have ∑ f o s = ∑ f o t.
LA - eng
KW - quotient order; ordered finite sequences
UR - http://eudml.org/doc/288462
ER -