@MISC{ORDERS_5.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg Universit in Mayence, Germany},
  TITLE = {About Quotient Orders and Ordering Sequences},
  ACKNOWLEDGEMENT = {I thank Dr. Adam Grabowski for his encouragement and the team behind {\tt     mus@mizar.uwb.edu.pl} for their fast and helpful replies to my beginner's questions},
  SECTION1 = {Preliminaries},
  SECTION2 = {Orders},
  SECTION3 = {Quotient Order},
  SECTION4 = {Ordering Finite Sequences},
  DAY = {27},
  MONTH = {June},
  YEAR = {2017},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {In preparation for the formulization of lotteries as given in \cite{MSZ}, this article closes     some gaps in the 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$ holds. This    concept was first introduced into the MML in \cite{DICKSON.ABS} and that work is incorporated here.        Furthermore given a set $A$, partitio
  finite-support function $f:A\rightarrow\mathbb  {R}$, a function
  $\sum_f : D \rightarrow\mathbb{R}, \sum_f (X) = \sum_{x\in 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:
  \[\sum_{x\in A} f(x) = \sum_{X\in D}\sum_f (X) \left(= \sum_{X\in D}\sum_{x\in X} f(x)\right)\]
   After that (weakly-)ascending/descending finite sequences (based on \cite{FINSEQ_1.ABS}) are introduced,   in analogous notation to their infinite counterparts introduced in \cite{WELLFND1.ABS}
  and \cite{DICKSON.ABS}. The second main result is any finite subset of any transitive
  connected relational structure can be sorted as a ascending or descending finite sequence, thus       generalizing the results from \cite{RFINSEQ2.ABS}, where finite sequence of real numbers where 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.\par
  Additionally, some auxiliary theorems are provided, e.g. two schemes to find a smallest or 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 \subseteq \rng s$, and a function $f:X\rightarrow\mathbb{R}$ such that $f$ is zero
  for every $x\in\rng s\setminus\rng t$, we have $\sum f\circ s = \sum f\circ t$.}}

@BOOK{MSZ,
  AUTHOR = {Maschler, Michael&datl=1927-2008 ; Solan, Eilon ; Zamir, Shmuel},
  TITLE = {Game theory},
  ADRESS = {Cambridge [u.a.]},
  PUBLISHER = {Cambridge Univ. Press},
  YEAR = {2013},
  ISBN = {978-1-107-00548-8 ; 1-107-00548-5},
  PAGES = {XXVI, 979 S.},
  URL = {http://assets.cambridge.org/97811070/05488/cover/9781107005488.jpg ; http://scans.hebis.de/HEBCGI/show.pl?32611138_toc.pdf},
}
