This formalization includes properties and definitions about orders, such as abstract orders, Lattices, fix points, etc.
| Theorem | Location | PVS Name | Contributors |
|---|---|---|---|
| Schroeder-Bernstein Theorem | orders@set_antinsymmetric |
inj_inj_bij |
Jerry James |
- Alfons Geser, HTWK Leipzig, Germany
- Bruno Dutertre, SRI, USA
- Jerry James, Utah State University, USA
- César Muñoz, NASA, USA
- Mariano Moscato, NIA & NASA, USA
- Anthony Narkawicz, NASA, USA
- Marco A. Feliú, NIA & NASA, USA
- Sam Owre, SRI, USA
- César Muñoz, NASA, USA
