isEmbedding_natCast — Mathlib

English

The natural embedding of ℕ into ℕ∞ is an embedding of ordered sets (an order-embedding).

Русский

Встраивание ℕ в ℕ∞ сохраняет порядок и вводит инъекцию (хорошо вложено по порядку).

LaTeX

$$$$\\text{IsEmbedding}(\\uparrow: \\mathbb{N} \\to \\mathbb{N}_{\\infty}).$$$$

Lean4

theorem isEmbedding_natCast : IsEmbedding ((↑) : ℕ → ℕ∞) :=
  Nat.strictMono_cast.isEmbedding_of_ordConnected <| range_natCast ▸ ordConnected_Iio

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