Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-23 11:46 1ed3a113

View on Github →

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.

Estimated changes

Modified src/model_theory/order.lean

added def first_order.language.DLO

added def first_order.language.densely_ordered_sentence

deleted def first_order.language.is_ordered_structure

deleted theorem first_order.language.is_ordered_structure_iff

added def first_order.language.linear_order_theory

added def first_order.language.no_bot_order_sentence

added def first_order.language.no_top_order_sentence

added def first_order.language.ordered_structure

added theorem first_order.language.ordered_structure_iff

added def first_order.language.partial_order_theory

added def first_order.language.preorder_theory

modified theorem first_order.language.realize_no_bot_order

modified theorem first_order.language.realize_no_bot_order_iff

modified theorem first_order.language.realize_no_top_order

modified theorem first_order.language.realize_no_top_order_iff

modified theorem first_order.language.rel_map_le_symb

modified theorem first_order.language.term.realize_le

modified theorem first_order.language.term.realize_lt