<abstract xmlns="http://www.w3.org/1999/xhtml">In preparation for the formalization in Mizar [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_004_w2aab3b7b4b1b6b1ab1ab4Aa">4</xref>] of lotteries as given in [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_014_w2aab3b7b4b1b6b1ab1ac14Aa">14</xref>], 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 <italic>x, y</italic> of a preorder as equivalent if <italic>x</italic> ⩽ <italic>y</italic> and <italic>y</italic> ⩽ <italic>x</italic>. This concept is known (see e.g. chapter 5 of [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>]) and was first introduced into the MML in [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_013_w2aab3b7b4b1b6b1ab1ac13Aa">13</xref>] and that work is incorporated here. Furthermore given a set <italic>A</italic>, partition <italic>D</italic> of <italic>A</italic> and a finite-support function <italic>f</italic> : <italic>A →</italic> ℝ, a function Σ<italic>f</italic> : <italic>D →</italic> ℝ, Σ<italic>f</italic> (<italic>X</italic>)= ∑<italic>x</italic>∈<italic>X</italic><italic>f</italic>(<italic>x</italic>) can be defined as some kind of natural “restriction” from <italic>f</italic> to <italic>D</italic>. The first main result of this article can then be formulated as:
<disp-formula><alternatives><graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2017-0012_eq_001.png"></graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><mstyle><munder><mo>∑</mo><mrow><mi>x</mi><mo>∈</mo><mi>A</mi></mrow></munder><mrow><mi>f</mi><mo>(</mo><mi>x</mi><mo>)</mo></mrow></mstyle><mo>=</mo><mstyle><munder><mo>∑</mo><mrow><mi>X</mi><mo>∈</mo><mi>D</mi></mrow></munder><mrow><msub><mo>Σ</mo><mi>f</mi></msub><mo>(</mo><mi>X</mi><mo>)</mo><mrow><mo>(</mo><mrow><mo>=</mo><mstyle><munder><mo>∑</mo><mrow><mi>X</mi><mo>∈</mo><mi>D</mi></mrow></munder><mrow><mstyle><munder><mo>∑</mo><mrow><mi>x</mi><mo>∈</mo><mi>X</mi></mrow></munder><mrow><mi>f</mi><mo>(</mo><mi>x</mi><mo>)</mo></mrow></mstyle></mrow></mstyle></mrow><mo>)</mo></mrow></mrow></mstyle></mrow></math><tex-math>$$\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)} $$</tex-math></alternatives></disp-formula>After that (weakly) ascending/descending finite sequences (based on [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_003_w2aab3b7b4b1b6b1ab1ab3Aa">3</xref>]) are introduced, in analogous notation to their infinite counterparts introduced in [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_018_w2aab3b7b4b1b6b1ab1ac18Aa">18</xref>] and [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_013_w2aab3b7b4b1b6b1ab1ac13Aa">13</xref>].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 [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_016_w2aab3b7b4b1b6b1ab1ac16Aa">16</xref>], 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. [<xref ref-type="bibr" rid="j_forma-2017-0012_ref_010_w2aab3b7b4b1b6b1ab1ac10Aa">10</xref>]).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 <italic>s, t</italic> on a set <italic>X</italic>, such that rng <italic>t</italic> ⊆ rng <italic>s</italic>, and a function <italic>f</italic> : <italic>X →</italic> ℝ such that <italic>f</italic> is zero for every <italic>x</italic> ∈ rng <italic>s \</italic> rng <italic>t</italic>, we have ∑ <italic>f</italic> o <italic>s</italic> = ∑ <italic>f</italic> o <italic>t</italic>.</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∈Xf(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.

About Quotient Orders and Ordering Sequences

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"About Quotient Orders and Ordering Sequences"}

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)...

About Quotient Orders and Ordering Sequences

Published Online: Sep 23, 2017

Page range: 121 - 139

Received: Jun 27, 2017

DOI: https://doi.org/10.1515/forma-2017-0012

Keywords
quotient order, ordered finite sequences

© 2017 Sebastian Koch, published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

About Quotient Orders and Ordering Sequences

Published Online: Sep 23, 2017

Page range: 121 - 139

Received: Jun 27, 2017

DOI: https://doi.org/10.1515/forma-2017-0012

Keywordsquotient order, ordered finite sequences

© 2017 Sebastian Koch, published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Keywords
quotient order, ordered finite sequences