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) regarding relational structures. The quotient order is introduced by the equivalence relation identifying two elements x, y of a preorder as equivale...

Full description

Bibliographic Details
Main Author: Koch Sebastian
Format: Article
Language:English
Published: Sciendo 2017-07-01
Series:Formalized Mathematics
Subjects:
Online Access:https://doi.org/10.1515/forma-2017-0012