mk_lt_mk — Mathlib

English

The strict order on ℕ⁺ matches the strict order on ℕ under the embedding: ⟨n, hn⟩ < ⟨k, hk⟩ iff n < k.

Русский

Строгий порядок на ℕ⁺ совпадает со строгим порядком на ℕ через вложение: ⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k.

LaTeX

$$$ (n k : \\mathbb{N}) (hn : 0 < n) (hk : 0 < k),\\; \\left(\\langle n, hn \\rangle \\lt \\langle k, hk \\rangle \\right) \\iff n < k.$$$

Lean4

theorem mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : (⟨n, hn⟩ : ℕ+) < ⟨k, hk⟩ ↔ n < k := by simp

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