strictMono — Mathlib

English

If f is an injective order-preserving map between ordered structures, then f is strictly monotone.

Русский

Если отображение f между упорядоченными структурами сохраняет порядок и инъективно, тогда оно строго монотонно.

LaTeX

$$$ \text{StrictMono } f $$$

Lean4

theorem strictMono [EmbeddingLike F M N] [PartialOrder M] [L.OrderedStructure M] [PartialOrder N] [L.OrderedStructure N]
    (f : F) : StrictMono f :=
  (HomClass.monotone f).strictMono_of_injective (EmbeddingLike.injective f)

Похожие утверждения