natGT — Mathlib

English

From a strictly r-decreasing sequence, we obtain a swap of natLT that yields an embedding for the order GT on ℕ.

Русский

Из строго убывающей по r последовательности следует вложение из ℕ в α по порядку GT.

LaTeX

$$$ \\text{natGT}(f,H) : (\\langle \\mathbb{N},>\\rangle) \\hookrightarrow_r (\\alpha,r). $$$

Lean4

/-- If `f` is a strictly `r`-decreasing sequence, then this returns `f` as an order embedding. -/
def natGT (f : ℕ → α) (H : ∀ n : ℕ, r (f (n + 1)) (f n)) : ((· > ·) : ℕ → ℕ → Prop) ↪r r :=
  haveI := IsStrictOrder.swap r
  RelEmbedding.swap (natLT f H)

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