mathlib

1ed3a113 - feat(model_theory/order): Renames and generalizes notation about ordered structures (#17870)

feat(model_theory/order): Renames and generalizes notation about ordered structures (#17870) Generalizes the definition of first-order sentences and theories about orders to work in ordered languages rather than just the one-symbol language `language.order`. Renames these sentences and theories accordingly: for instance, the dot notation `L.preorder_theory` is the theory of preordered `L`-structures, which requires that `preorder_theory` be directly in the namespace `first_order.language`.