Commit 2022-04-08 12:12 710fe040

View on Github →

feat(model_theory/order): Defines ordered languages and structures (#13088) Defines ordered languages and ordered structures Defines the theories of pre-, partial, and linear orders, shows they are modeled by the respective structures.

Estimated changes

Created src/model_theory/order.lean

added def first_order.language.is_ordered_structure

added def first_order.language.order_Lhom

added theorem first_order.language.order_Lhom_order

added def first_order.language.term.le