Order

📁 Source: Mathlib/ModelTheory/Order.lean

Statistics

Metric	Count
Definitions `IsOrdered`, `leSymb`, `OrderedStructure`, `le`, `lt`, `decidableLEOfStructure`, `denselyOrderedSentence`, `dlo`, `instDecidableEqOrderRel`, `decEq`, `instIsOrderedOrder`, `instIsRelationalOrder`, `leOfStructure`, `linearOrderOfModels`, `linearOrderTheory`, `noBotOrderSentence`, `noTopOrderSentence`, `instUniqueSigmaNatRelations`, `instUniqueSymbols`, `orderLHom`, `orderRel`, `orderStructure`, `partialOrderOfModels`, `partialOrderTheory`, `preorderOfModels`, `preorderTheory`, `instIsOrdered`	27
Theorems `monotone`, `strictMono`, `relMap_leSymb`, `toOrderIsoClass`, `realize_le`, `realize_lt`, `aleph0_categorical_dlo`, `denselyOrdered_of_dlo`, `dlo_age`, `dlo_isComplete`, `dlo_isExtensionPair`, `instInfiniteOfModelDloOrderOfNonempty`, `instIsExpansionOnOrderLHomOfOrderedStructureOrder`, `instIsUniversalLinearOrderTheory`, `instIsUniversalPartialOrderTheory`, `instIsUniversalPreorderTheory`, `instModelLinearOrderTheoryOfDlo`, `instModelPartialOrderTheoryOfLinearOrderTheory`, `instModelPreorderTheoryOfPartialOrderTheory`, `instOrderedStructure`, `instOrderedStructureOfOrderOfIsExpansionOnOrderLHom`, `instOrderedStructureSubtypeMemSubstructure`, `isFraisseLimit_of_countable_nonempty_dlo`, `isFraisse_finite_linear_order`, `model_dlo`, `model_linearOrder`, `model_partialOrder`, `model_preorder`, `noBotOrder_of_dlo`, `noTopOrder_of_dlo`, `card_eq_one`, `forall_relations`, `instHomClassOfOrderHomClass`, `instIsEmptyRelationsOfNatNat`, `instStrongHomClassOfOrderIsoClass`, `instStrongHomClassOrderEmbedding`, `instSubsingleton`, `relation_eq_leSymb`, `orderLHom_leSymb`, `orderLHom_onFunction`, `orderLHom_onRelation`, `orderLHom_order`, `orderedStructure_iff`, `realize_denselyOrdered`, `realize_denselyOrdered_iff`, `realize_noBotOrder`, `realize_noBotOrder_iff`, `realize_noTopOrder`, `realize_noTopOrder_iff`	49
Total	76

FirstOrder.Language

Definitions

Name	Category	Theorems
`IsOrdered` 📖	CompData	—
`OrderedStructure` 📖	CompData	4 math math: `instOrderedStructureOfOrderOfIsExpansionOnOrderLHom`, `instOrderedStructureSubtypeMemSubstructure`, `instOrderedStructure`, `orderedStructure_iff`
`decidableLEOfStructure` 📖	CompOp	—
`denselyOrderedSentence` 📖	CompOp	2 math math: `realize_denselyOrdered_iff`, `realize_denselyOrdered`
`dlo` 📖	CompOp	3 math math: `dlo_isComplete`, `model_dlo`, `aleph0_categorical_dlo`
`instDecidableEqOrderRel` 📖	CompOp	—
`instIsOrderedOrder` 📖	CompOp	8 math math: `orderLHom_leSymb`, `dlo_age`, `order.relation_eq_leSymb`, `orderLHom_order`, `isFraisse_finite_linear_order`, `isFraisseLimit_of_countable_nonempty_dlo`, `dlo_isComplete`, `aleph0_categorical_dlo`
`instIsRelationalOrder` 📖	CompOp	1 math math: `orderLHom_onFunction`
`leOfStructure` 📖	CompOp	1 math math: `instOrderedStructure`
`linearOrderOfModels` 📖	CompOp	—
`linearOrderTheory` 📖	CompOp	6 math math: `instIsUniversalLinearOrderTheory`, `dlo_age`, `instModelLinearOrderTheoryOfDlo`, `isFraisse_finite_linear_order`, `isFraisseLimit_of_countable_nonempty_dlo`, `model_linearOrder`
`noBotOrderSentence` 📖	CompOp	2 math math: `realize_noBotOrder_iff`, `realize_noBotOrder`
`noTopOrderSentence` 📖	CompOp	2 math math: `realize_noTopOrder_iff`, `realize_noTopOrder`
`orderLHom` 📖	CompOp	6 math math: `orderLHom_leSymb`, `orderLHom_order`, `instIsExpansionOnOrderLHomOfOrderedStructureOrder`, `orderLHom_onRelation`, `orderedStructure_iff`, `orderLHom_onFunction`
`orderRel` 📖	CompData	—
`orderStructure` 📖	CompOp	—
`partialOrderOfModels` 📖	CompOp	—
`partialOrderTheory` 📖	CompOp	3 math math: `model_partialOrder`, `instModelPartialOrderTheoryOfLinearOrderTheory`, `instIsUniversalPartialOrderTheory`
`preorderOfModels` 📖	CompOp	—
`preorderTheory` 📖	CompOp	3 math math: `model_preorder`, `instModelPreorderTheoryOfPartialOrderTheory`, `instIsUniversalPreorderTheory`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aleph0_categorical_dlo` 📖	mathematical	—	`Cardinal.Categorical` `order` `Cardinal.aleph0` `dlo` `instIsOrderedOrder`	—	`Cardinal.denumerable_iff` `IsFraisseLimit.nonempty_equiv` `Countable.countable_functions` `Finite.to_countable` `Finite.of_fintype` `Encodable.countable` `isFraisseLimit_of_countable_nonempty_dlo` `Theory.ModelType.nonempty'` `Theory.ModelType.is_model`
`denselyOrdered_of_dlo` 📖	mathematical	—	`DenselyOrdered` `Preorder.toLT`	—	`realize_denselyOrdered_iff` `Theory.realize_sentence_of_mem` `Set.union_insert` `Set.union_singleton`
`dlo_age` 📖	mathematical	—	`age` `order` `setOf` `CategoryTheory.Bundled` `Structure` `Finite` `CategoryTheory.Bundled.α` `Theory.Model` `CategoryTheory.Bundled.structure` `linearOrderTheory` `instIsOrderedOrder`	—	`age.eq_1` `Set.ext` `Structure.FG.finite` `Theory.IsUniversal.models_of_embedding` `instIsUniversalLinearOrderTheory` `instModelLinearOrderTheoryOfDlo` `Structure.FG.of_finite` `RelEmbedding.instEmbeddingLike` `order.instStrongHomClassOrderEmbedding` `instOrderedStructure` `nonempty_orderEmbedding_of_finite_infinite` `instInfiniteOfModelDloOrderOfNonempty`
`dlo_isComplete` 📖	mathematical	—	`Theory.IsComplete` `order` `dlo` `instIsOrderedOrder`	—	`Cardinal.Categorical.isComplete` `aleph0_categorical_dlo` `le_rfl` `order.card_eq_one` `Cardinal.lift_id` `model_dlo` `instOrderedStructure` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instIsStrictOrderedRing` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `instNoBotOrderOfNoMinOrder` `instNoMinOrderOfNontrivial` `instInfiniteOfModelDloOrderOfNonempty` `Theory.ModelType.is_model` `Theory.ModelType.nonempty'`
`dlo_isExtensionPair` 📖	mathematical	—	`IsExtensionPair` `order`	—	`le_sup_right` `isExtensionPair_iff_exists_embedding_closure_singleton_sup` `instModelLinearOrderTheoryOfDlo` `denselyOrdered_of_dlo` `instOrderedStructure` `noBotOrder_of_dlo` `noTopOrder_of_dlo` `NoBotOrder.to_noMinOrder` `NoTopOrder.to_noMaxOrder` `Structure.FG.finite` `Substructure.fg_iff_structure_fg` `Finset.subset_insert` `Set.Finite.coe_toFinset` `HomClass.strictMono` `StrongHomClass.homClass` `Embedding.strongHomClass` `Embedding.embeddingLike` `instOrderedStructureSubtypeMemSubstructure` `Order.exists_orderEmbedding_insert` `Finset.coe_insert` `Substructure.closure_insert` `Substructure.closure_eq` `LowerAdjoint.closure_eq_self_of_mem_closed` `Substructure.mem_closed_of_isRelational` `RelEmbedding.instEmbeddingLike` `order.instStrongHomClassOrderEmbedding` `Embedding.ext`
`instInfiniteOfModelDloOrderOfNonempty` 📖	mathematical	—	`Infinite`	—	`order.instIsEmptyRelationsOfNatNat` `embedding_from_cg` `Structure.cg_of_countable` `Encodable.countable` `dlo_isExtensionPair` `model_linearOrder` `instOrderedStructure` `Infinite.of_injective` `CharZero.infinite` `Rat.instCharZero` `Embedding.injective`
`instIsExpansionOnOrderLHomOfOrderedStructureOrder` 📖	mathematical	—	`LHom.IsExpansionOn` `order` `orderLHom`	—	`order.relation_eq_leSymb`
`instIsUniversalLinearOrderTheory` 📖	mathematical	—	`Theory.IsUniversal` `linearOrderTheory`	—	`Theory.IsUniversal.insert` `instIsUniversalPartialOrderTheory` `Relations.isUniversal_total`
`instIsUniversalPartialOrderTheory` 📖	mathematical	—	`Theory.IsUniversal` `partialOrderTheory`	—	`Theory.IsUniversal.insert` `instIsUniversalPreorderTheory` `Relations.isUniversal_antisymmetric`
`instIsUniversalPreorderTheory` 📖	mathematical	—	`Theory.IsUniversal` `preorderTheory`	—	`Relations.isUniversal_reflexive` `Relations.isUniversal_transitive`
`instModelLinearOrderTheoryOfDlo` 📖	mathematical	—	`Theory.Model` `linearOrderTheory`	—	`Theory.Model.mono` `Set.subset_union_left`
`instModelPartialOrderTheoryOfLinearOrderTheory` 📖	mathematical	—	`Theory.Model` `partialOrderTheory`	—	`Theory.Model.mono` `Set.subset_insert`
`instModelPreorderTheoryOfPartialOrderTheory` 📖	mathematical	—	`Theory.Model` `preorderTheory`	—	`Theory.Model.mono` `Set.subset_insert`
`instOrderedStructure` 📖	mathematical	—	`OrderedStructure` `leOfStructure`	—	`Fin.cons_zero`
`instOrderedStructureOfOrderOfIsExpansionOnOrderLHom` 📖	mathematical	—	`OrderedStructure`	—	`orderLHom_leSymb` `LHom.IsExpansionOn.map_onRelation` `OrderedStructure.relMap_leSymb`
`instOrderedStructureSubtypeMemSubstructure` 📖	mathematical	—	`OrderedStructure` `Substructure` `SetLike.instMembership` `Substructure.instSetLike` `Substructure.inducedStructure`	—	`OrderedStructure.relMap_leSymb`
`isFraisseLimit_of_countable_nonempty_dlo` 📖	mathematical	—	`IsFraisseLimit` `order` `setOf` `CategoryTheory.Bundled` `Structure` `Finite` `CategoryTheory.Bundled.α` `Theory.Model` `CategoryTheory.Bundled.structure` `linearOrderTheory` `instIsOrderedOrder` `Countable.countable_functions` `Finite.to_countable` `Symbols` `Finite.of_fintype` `Unique.fintype` `order.instUniqueSymbols`	—	`Countable.countable_functions` `Finite.to_countable` `Finite.of_fintype` `isUltrahomogeneous_iff_IsExtensionPair` `Structure.cg_of_countable` `dlo_isExtensionPair` `instModelLinearOrderTheoryOfDlo` `dlo_age`
`isFraisse_finite_linear_order` 📖	mathematical	—	`IsFraisse` `order` `setOf` `CategoryTheory.Bundled` `Structure` `Finite` `CategoryTheory.Bundled.α` `Theory.Model` `CategoryTheory.Bundled.structure` `linearOrderTheory` `instIsOrderedOrder`	—	`IsFraisseLimit.isFraisse` `Countable.countable_functions` `Finite.to_countable` `Finite.of_fintype` `Encodable.countable` `isFraisseLimit_of_countable_nonempty_dlo` `model_dlo` `instOrderedStructure` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instIsStrictOrderedRing` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `instNoBotOrderOfNoMinOrder` `instNoMinOrderOfNontrivial`
`model_dlo` 📖	mathematical	—	`Theory.Model` `dlo`	—	`Set.union_insert` `Set.union_singleton`
`model_linearOrder` 📖	mathematical	—	`Theory.Model` `linearOrderTheory`	—	`LE.total`
`model_partialOrder` 📖	mathematical	—	`Theory.Model` `partialOrderTheory`	—	`instAntisymmLe`
`model_preorder` 📖	mathematical	—	`Theory.Model` `preorderTheory`	—	`le_refl` `le_trans`
`noBotOrder_of_dlo` 📖	mathematical	—	`NoBotOrder`	—	`realize_noBotOrder_iff` `Theory.realize_sentence_of_mem` `Set.union_insert` `Set.union_singleton`
`noTopOrder_of_dlo` 📖	mathematical	—	`NoTopOrder`	—	`realize_noTopOrder_iff` `Theory.realize_sentence_of_mem` `Set.union_insert` `Set.union_singleton`
`orderLHom_leSymb` 📖	mathematical	—	`LHom.onRelation` `order` `orderLHom` `IsOrdered.leSymb` `instIsOrderedOrder`	—	—
`orderLHom_onFunction` 📖	mathematical	—	`LHom.onFunction` `order` `orderLHom` `isEmptyElim` `Functions` `instIsRelationalOrder`	—	—
`orderLHom_onRelation` 📖	mathematical	—	`LHom.onRelation` `order` `orderLHom` `Relations` `IsOrdered.leSymb`	—	—
`orderLHom_order` 📖	mathematical	—	`orderLHom` `order` `instIsOrderedOrder` `LHom.id`	—	`LHom.funext` `IsEmpty.instSubsingleton` `order.instSubsingleton`
`orderedStructure_iff` 📖	mathematical	—	`OrderedStructure` `LHom.IsExpansionOn` `order` `orderLHom`	—	`instIsExpansionOnOrderLHomOfOrderedStructureOrder` `instOrderedStructureOfOrderOfIsExpansionOnOrderLHom`
`realize_denselyOrdered` 📖	mathematical	—	`Sentence.Realize` `denselyOrderedSentence`	—	`realize_denselyOrdered_iff`
`realize_denselyOrdered_iff` 📖	mathematical	—	`Sentence.Realize` `denselyOrderedSentence` `DenselyOrdered` `Preorder.toLT`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `exists_between`
`realize_noBotOrder` 📖	mathematical	—	`Sentence.Realize` `noBotOrderSentence`	—	`realize_noBotOrder_iff`
`realize_noBotOrder_iff` 📖	mathematical	—	`Sentence.Realize` `noBotOrderSentence` `NoBotOrder`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `NoBotOrder.exists_not_ge`
`realize_noTopOrder` 📖	mathematical	—	`Sentence.Realize` `noTopOrderSentence`	—	`realize_noTopOrder_iff`
`realize_noTopOrder_iff` 📖	mathematical	—	`Sentence.Realize` `noTopOrderSentence` `NoTopOrder`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `NoTopOrder.exists_not_le`

FirstOrder.Language.HomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monotone` 📖	mathematical	—	`Monotone` `DFunLike.coe`	—	`map_rel`
`strictMono` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `DFunLike.coe`	—	`Monotone.strictMono_of_injective` `monotone` `EmbeddingLike.injective`

FirstOrder.Language.IsOrdered

Definitions

Name	Category	Theorems
`leSymb` 📖	CompOp	4 math math: `FirstOrder.Language.orderLHom_leSymb`, `FirstOrder.Language.order.relation_eq_leSymb`, `FirstOrder.Language.OrderedStructure.relMap_leSymb`, `FirstOrder.Language.orderLHom_onRelation`

FirstOrder.Language.OrderedStructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`relMap_leSymb` 📖	mathematical	—	`FirstOrder.Language.Structure.RelMap` `FirstOrder.Language.IsOrdered.leSymb`	—	—

FirstOrder.Language.StrongHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toOrderIsoClass` 📖	mathematical	—	`OrderIsoClass`	—	`map_rel`

FirstOrder.Language.Term

Definitions

Name	Category	Theorems
`le` 📖	CompOp	1 math math: `realize_le`
`lt` 📖	CompOp	1 math math: `realize_lt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_le` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.Realize` `le` `realize`	—	`Matrix.cons_val_fin_one`
`realize_lt` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.Realize` `lt` `Preorder.toLT` `realize`	—	—

FirstOrder.Language.instDecidableEqOrderRel

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

FirstOrder.Language.order

Definitions

Name	Category	Theorems
`instUniqueSigmaNatRelations` 📖	CompOp	—
`instUniqueSymbols` 📖	CompOp	1 math math: `FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq_one` 📖	mathematical	—	`FirstOrder.Language.card` `FirstOrder.Language.order` `Cardinal` `Cardinal.instOne`	—	`Cardinal.mk_fintype` `Fintype.card_unique` `Nat.cast_one`
`forall_relations` 📖	mathematical	—	`FirstOrder.Language.orderRel.le`	—	—
`instHomClassOfOrderHomClass` 📖	mathematical	—	`FirstOrder.Language.HomClass` `FirstOrder.Language.order`	—	`relation_eq_leSymb` `RelHomClass.map_rel`
`instIsEmptyRelationsOfNatNat` 📖	mathematical	—	`IsEmpty` `FirstOrder.Language.Relations` `FirstOrder.Language.order`	—	—
`instStrongHomClassOfOrderIsoClass` 📖	mathematical	—	`FirstOrder.Language.StrongHomClass` `FirstOrder.Language.order` `EquivLike.toFunLike`	—	`relation_eq_leSymb`
`instStrongHomClassOrderEmbedding` 📖	mathematical	—	`FirstOrder.Language.StrongHomClass` `FirstOrder.Language.order` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`relation_eq_leSymb`
`instSubsingleton` 📖	mathematical	—	`FirstOrder.Language.Relations` `FirstOrder.Language.order`	—	—
`relation_eq_leSymb` 📖	mathematical	—	`FirstOrder.Language.IsOrdered.leSymb` `FirstOrder.Language.order` `FirstOrder.Language.instIsOrderedOrder`	—	—

FirstOrder.Language.sum

Definitions

Name	Category	Theorems
`instIsOrdered` 📖	CompOp	—

---

← Back to Index