Commit 2024-09-05 13:49 66787e8f

View on Github →

feat(ModelTheory/Order): From order to structure and back (#16373) Makes FirstOrder.Language.orderStructure a def instead of an instance Provides defs to turn L.Structures in ordered languages modelling the relevant theories into LE, Preorder, PartialOrder, and LinearOrder.

Estimated changes

Modified Mathlib/ModelTheory/Order.lean

modified theorem FirstOrder.Language.Term.realize_lt

added def FirstOrder.Language.leOfStructure

added def FirstOrder.Language.linearOrderOfModels

added theorem FirstOrder.Language.order.relation_eq_leSymb

modified def FirstOrder.Language.orderLHom

deleted theorem FirstOrder.Language.orderLHom_apply

added def FirstOrder.Language.orderStructure

modified theorem FirstOrder.Language.orderedStructure_iff

added def FirstOrder.Language.partialOrderOfModels

added def FirstOrder.Language.preorderOfModels

modified theorem FirstOrder.Language.realize_noBotOrder

modified theorem FirstOrder.Language.realize_noBotOrder_iff

modified theorem FirstOrder.Language.realize_noTopOrder

modified theorem FirstOrder.Language.realize_noTopOrder_iff

deleted theorem FirstOrder.Language.relMap_leSymb