### 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

- Mathematics/Order

### Session Szpilrajn

- Szpilrajn

### Used by

- Lyndon words

## Cite

×

Szpilrajn-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jul 28, 2019 : Isabelle2019