# About Quotient Orders and Ordering Sequences

Formalized Mathematics (2017)

- Volume: 25, Issue: 2, page 121-139
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topSebastian 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 -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.