natLT — Mathlib

English

Given a strictly r-increasing sequence f: ℕ → α, there is an order-embedding of (ℕ, <) into (α, r).

Русский

Дана строго возрастающая по r последовательность f: ℕ → α, существует вложение (ℕ, <) → α, сохраняющее порядок.

LaTeX

$$$ \\text{natLT}(f,H) : (\\langle \\mathbb{N},< \\rangle) \\hookrightarrow_r (\\alpha,r) $$$

Lean4

/-- If `f` is a strictly `r`-increasing sequence, then this returns `f` as an order embedding. -/
def natLT (f : ℕ → α) (H : ∀ n : ℕ, r (f n) (f (n + 1))) : ((· < ·) : ℕ → ℕ → Prop) ↪r r :=
  ofMonotone f <| Nat.rel_of_forall_rel_succ_of_lt r H

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