[isabelle] New AFP entry: Szpilrajn Extension Theorem



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!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.