Theorems · Theorem · logic and foundations

FirstOrder.Language.orderLHom_onRelation

∀ (L : FirstOrder.Language) [inst : L.IsOrdered] (x : ℕ) (x_1 : FirstOrder.Language.order.Relations x),
  L.orderLHom.onRelation x_1 =
    match x, x_1 with
    | .(2), FirstOrder.Language.orderRel.le => FirstOrder.Language.leSymb

Defined in: Mathlib.ModelTheory.Order
Cited by: 0 results in Mathlib
Foundations: Depth 18 from the axioms · uses no axioms
Assumes: FirstOrder.Language.IsOrdered

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

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.Relationsstatement and proof · cited by 147
FirstOrder.Language.LHom.onRelationstatement and proof · cited by 27
FirstOrder.Language.IsOrderedstatement and proof · cited by 19
FirstOrder.Language.orderstatement and proof · cited by 14
FirstOrder.Language.IsOrdered.leSymbstatement · cited by 6
FirstOrder.Language.orderLHomstatement and proof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.