Structures · Logic and sets
FirstOrder.Language.OrderedStructure
A structure is ordered if its language has a ≤ symbol whose interpretation is ≤.
- Defined in
- Mathlib.ModelTheory.Order
- Shape
- 2 explicit arguments · adds relMap_leSymb
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- FirstOrder.Language.realize_noBotOrder_iff
- FirstOrder.Language.realize_noTopOrder_iff
- FirstOrder.Language.realize_denselyOrdered_iff
- FirstOrder.Language.denselyOrdered_of_dlo
- FirstOrder.Language.HomClass.strictMono
- FirstOrder.Language.noBotOrder_of_dlo
- FirstOrder.Language.HomClass.monotone
- FirstOrder.Language.noTopOrder_of_dlo
- FirstOrder.Language.orderedStructure_iff
- FirstOrder.Language.Term.realize_le
- FirstOrder.Language.instIsExpansionOnOrderLHomOfOrderedStructureOrder
- FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass
- FirstOrder.Language.model_partialOrder
- FirstOrder.Language.instOrderedStructureSubtypeMemSubstructure
- FirstOrder.Language.realize_noTopOrder
- FirstOrder.Language.order.instStrongHomClassOrderEmbedding
- FirstOrder.Language.realize_denselyOrdered
- FirstOrder.Language.StrongHomClass.toOrderIsoClass
- FirstOrder.Language.OrderedStructure.relMap_leSymb
- FirstOrder.Language.model_linearOrder
- FirstOrder.Language.model_dlo
- FirstOrder.Language.realize_noBotOrder
- FirstOrder.Language.model_preorder
- FirstOrder.Language.instOrderedStructureOfOrderOfIsExpansionOnOrderLHom
- FirstOrder.Language.order.instHomClassOfOrderHomClass
- FirstOrder.Language.Term.realize_lt
Ancestors0
No ancestors.