What is it about?
Definition and basic properties of quotient orders as well as the existence of increasing and decreasing sequences of finite subsets of an ordered set.
Featured Image
Why is it important?
This paper closes some gaps in the Mizar Mathematical Library. The quotient order is important for the theory of lotteries and the existence theorems for ordered sequences have a couple of applications.
Perspectives
This was my first paper to be submitted and published. I thank Adam Grabowski and the team behind the Mizar user service for helping me to learn and understand the Mizar language.
B.Sc. Sebastian Koch
Johannes Gutenberg Universitat Mainz
Read the Original
This page is a summary of: About Quotient Orders and Ordering Sequences, Formalized Mathematics, July 2017, De Gruyter,
DOI: 10.1515/forma-2017-0012.
You can read the full text:
Resources
Contributors
The following have contributed to this page
