Order Extension and Szpilrajn's Extension Theorem

Peter Zeller 📧 and Lukas Stevens 🌐

July 27, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry is concerned with the principle of order extension, i.e. the extension of an order relation to a total order relation. To this end, we prove a more general version of Szpilrajn's extension theorem employing terminology from the book "Consistency, Choice, and Rationality" by Bossert and Suzumura. We also formalize theorem 2.7 of their book.

License

BSD License

History

March 22, 2021
(by Lukas Stevens) generalise Szpilrajn's extension theorem and add material from the book "Consistency, Choice, and Rationality"

Topics

Session Szpilrajn

Used by

Cite

× 
@article{Szpilrajn-AFP,
  author  = {Peter Zeller and Lukas Stevens},
  title   = {Order Extension and Szpilrajn's Extension Theorem},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/Szpilrajn.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: