Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 08:46 670735fc

View on Github →

feat(model_theory/order): The theory of dense linear orders without endpoints (#13253) Defines the theory of dense linear orders without endpoints

Estimated changes

Modified src/model_theory/order.lean

modified def first_order.language.is_ordered_structure

added theorem first_order.language.is_ordered_structure_iff

added theorem first_order.language.order_Lhom_le_symb

added theorem first_order.language.realize_densely_ordered

added theorem first_order.language.realize_densely_ordered_iff

added theorem first_order.language.realize_no_bot_order

added theorem first_order.language.realize_no_bot_order_iff

added theorem first_order.language.realize_no_top_order

added theorem first_order.language.realize_no_top_order_iff

added theorem first_order.language.rel_map_le_symb

added def first_order.language.term.lt

added theorem first_order.language.term.realize_le

added theorem first_order.language.term.realize_lt