Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Szpilrajn Extension Theorem

Email Gateway (Aug 22 2022 at 20:07):

From: Tobias Nipkow <nipkow@in.tum.de>
Szpilrajn Extension Theorem
Peter Zeller

We formalize the Szpilrajn extension theorem, also known as order-extension
principal: Every strict partial order can be extended to a strict linear order.

https://www.isa-afp.org/entries/Szpilrajn.html

Enjoy!
smime.p7s

Last updated: Nov 21 2024 at 12:39 UTC