Theorems · Definition · logic and foundations
FirstOrder.Language.orderLHom
(L : FirstOrder.Language) → [L.IsOrdered] → FirstOrder.Language.order →ᴸ L
The language homomorphism sending the unique symbol ≤ of Language.order to ≤ in an ordered
language.
- Defined in
- Mathlib.ModelTheory.Order
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Functionsproof · cited by 153
- FirstOrder.Language.Relationsproof · cited by 147
- FirstOrder.Language.LHomstatement · cited by 66
- isEmptyElimproof · cited by 59
- FirstOrder.Language.IsOrderedstatement and proof · cited by 19
- FirstOrder.Language.orderstatement and proof · cited by 14
- FirstOrder.Language.IsOrdered.leSymbproof · cited by 6
Cited by5
Results whose statement or proof uses this declaration.
- FirstOrder.Language.orderedStructure_iffstatement and proof · cited by 0
- FirstOrder.Language.orderLHom_leSymbstatement · cited by 0
- FirstOrder.Language.orderLHom_onFunctionstatement and proof · cited by 0
- FirstOrder.Language.orderLHom_onRelationstatement and proof · cited by 0
- FirstOrder.Language.orderLHom_orderstatement and proof · cited by 0