feat(model_theory/order): Defines ordered languages and structures (#13088)
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.



Co-authored-by: Floris van Doorn <04eee3258902297ef5081ba8b0786f6ab1274795@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib