Theorems · Theorem · logic and foundations

FirstOrder.Language.HomClass.strictMono

∀ {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] [EmbeddingLike F M N]
  [inst_6 : PartialOrder M] [L.OrderedStructure M] [inst_8 : PartialOrder N] [L.OrderedStructure N] (f : F),
  StrictMono ⇑f

Defined in

Mathlib.ModelTheory.Order

Cited by

1 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext

Assumes

FirstOrder.Language.IsOrderedFirstOrder.Language.StructureFirstOrder.Language.StructureFunLikeFirstOrder.Language.HomClassEmbeddingLikePartialOrderFirstOrder.Language.OrderedStructurePartialOrderFirstOrder.Language.OrderedStructure