Theorems · Theorem · logic and foundations

FirstOrder.Language.HomClass.monotone

∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] {N : Type u_1}
  [inst_2 : L.Structure N] {F : Type u_2} [inst_3 : FunLike F M N] [L.HomClass F M N] [inst_5 : Preorder M]
  [L.OrderedStructure M] [inst_7 : Preorder N] [L.OrderedStructure N] (f : F), Monotone ⇑f

Defined in

Mathlib.ModelTheory.Order

Cited by

1 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext

Assumes

FirstOrder.Language.IsOrderedFirstOrder.Language.StructureFirstOrder.Language.StructureFunLikeFirstOrder.Language.HomClassPreorderFirstOrder.Language.OrderedStructurePreorderFirstOrder.Language.OrderedStructure