Theorems · Theorem · logic and foundations

FirstOrder.Language.StrongHomClass.toOrderIsoClass

∀ (L : FirstOrder.Language) [inst : L.IsOrdered] (M : Type u_1) [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] (N : Type u_2) [inst_4 : L.Structure N] [inst_5 : LE N] [L.OrderedStructure N] (F : Type u_3)
  [inst : EquivLike F M N] [L.StrongHomClass F M N], OrderIsoClass F M N

This is not an instance because it would form a loop with FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass. As both types are Props, it would only cause a slowdown.

Defined in

Mathlib.ModelTheory.Order

Cited by

0 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.IsOrderedFirstOrder.Language.StructureLEFirstOrder.Language.OrderedStructureFirstOrder.Language.StructureLEFirstOrder.Language.OrderedStructureEquivLikeFirstOrder.Language.StrongHomClass