Structures · Logic and sets
FirstOrder.Language.IsOrdered
A language is ordered if it has a symbol representing ≤.
- Defined in
- Mathlib.ModelTheory.Order
- Shape
- One type argument · adds leSymb
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- FirstOrder.Language.order
- FirstOrder.Language.sum
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- FirstOrder.Language.dlo
- FirstOrder.Language.linearOrderTheory
- FirstOrder.Language.IsOrdered.leSymb
- FirstOrder.Language.denselyOrderedSentence
- FirstOrder.Language.noTopOrderSentence
- FirstOrder.Language.orderLHom
- FirstOrder.Language.noBotOrderSentence
- FirstOrder.Language.linearOrderOfModels
- 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.Term.le
- FirstOrder.Language.noBotOrder_of_dlo
- FirstOrder.Language.HomClass.monotone
- FirstOrder.Language.Term.lt
- FirstOrder.Language.noTopOrder_of_dlo
- FirstOrder.Language.orderedStructure_iff
- FirstOrder.Language.Term.realize_le
- FirstOrder.Language.instIsExpansionOnOrderLHomOfOrderedStructureOrder
- FirstOrder.Language.decidableLEOfStructure
- FirstOrder.Language.model_partialOrder
- FirstOrder.Language.instOrderedStructureSubtypeMemSubstructure
- FirstOrder.Language.orderLHom_onRelation
- FirstOrder.Language.realize_noTopOrder
- FirstOrder.Language.realize_denselyOrdered
- FirstOrder.Language.StrongHomClass.toOrderIsoClass
- FirstOrder.Language.partialOrderTheory
- FirstOrder.Language.model_linearOrder
- FirstOrder.Language.instIsUniversalPreorderTheory
- FirstOrder.Language.model_dlo
- FirstOrder.Language.realize_noBotOrder
- FirstOrder.Language.model_preorder
- FirstOrder.Language.instModelLinearOrderTheoryOfDlo
- FirstOrder.Language.preorderOfModels
- FirstOrder.Language.partialOrderOfModels
- FirstOrder.Language.instOrderedStructureOfOrderOfIsExpansionOnOrderLHom
- FirstOrder.Language.instOrderedStructure
- FirstOrder.Language.orderLHom_onFunction
- FirstOrder.Language.orderLHom_leSymb
- FirstOrder.Language.instIsUniversalPartialOrderTheory
- FirstOrder.Language.leOfStructure
- FirstOrder.Language.instIsUniversalLinearOrderTheory
- FirstOrder.Language.preorderTheory
- FirstOrder.Language.instModelPreorderTheoryOfPartialOrderTheory
- FirstOrder.Language.instModelPartialOrderTheoryOfLinearOrderTheory
- FirstOrder.Language.Term.realize_lt
Ancestors0
No ancestors.