PL EN

Widoczny [Schowaj] Abstrakt
Liczba wyników
Czasopismo

## Formalized Mathematics

2017 | 25 | 2 | 121-139
Tytuł artykułu

### About Quotient Orders and Ordering Sequences

Autorzy
Treść / Zawartość
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
In preparation for the formalization in Mizar  of lotteries as given in , 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 ) and was first introduced into the MML in  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 ) are introduced, in analogous notation to their infinite counterparts introduced in  and . 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 , 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. ). 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.
Słowa kluczowe
EN
Kategorie tematyczne
Wydawca
Czasopismo
Rocznik
Tom
Numer
Strony
121-139
Opis fizyczny
Daty
wydano
2017-07-01
otrzymano
2017-06-27
online
2017-09-23
Twórcy
autor
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.