Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Tytuł: About Quotient Orders and Ordering Sequences
Autorzy: Koch, Sebastian
Słowa kluczowe: quotient order
ordered finite sequences
Data wydania: 2017
Data dodania: 8-lut-2018
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 25, Issue 2, Pages 121–139
Abstrakt: SummaryIn 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)) 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.
Afiliacja: Johannes Gutenberg University, Mainz, Germany
DOI: 10.1515/forma-2017-0012
ISSN: 1426-2630
e-ISSN: 1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2017, Volume 25, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2017-0012.pdf376,91 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons