About Quotient Orders and Ordering Sequences

• Main Author: Koch Sebastian
• Format: Article
• Language: English
• Published: Sciendo 2017-07-01
• Series: Formalized Mathematics
• Subjects: quotient order; ordered finite sequences; 06a05; 03b35
• Online Access: https://doi.org/10.1515/forma-2017-0012

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)} $$