Commit 2023-05-12 16:00 864fd0cb

View on Github →

feat: port ModelTheory.Order (#3911)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Order.lean

added def FirstOrder.Language.Term.le

added def FirstOrder.Language.Term.lt

added theorem FirstOrder.Language.Term.realize_le

added theorem FirstOrder.Language.Term.realize_lt

added def FirstOrder.Language.denselyOrderedSentence

added def FirstOrder.Language.dlo

added def FirstOrder.Language.linearOrderTheory

added def FirstOrder.Language.noBotOrderSentence

added def FirstOrder.Language.noTopOrderSentence

added def FirstOrder.Language.orderLHom

added theorem FirstOrder.Language.orderLHom_leSymb

added theorem FirstOrder.Language.orderLHom_order

added theorem FirstOrder.Language.orderedStructure_iff

added def FirstOrder.Language.partialOrderTheory

added def FirstOrder.Language.preorderTheory

added theorem FirstOrder.Language.realize_denselyOrdered

added theorem FirstOrder.Language.realize_denselyOrdered_iff

added theorem FirstOrder.Language.realize_noBotOrder

added theorem FirstOrder.Language.realize_noBotOrder_iff

added theorem FirstOrder.Language.realize_noTopOrder

added theorem FirstOrder.Language.realize_noTopOrder_iff

added theorem FirstOrder.Language.relMap_leSymb