ofNat_lt_ofNat — Mathlib

English

For m,n ∈ ℕ with NeZero, (ofNat(m) : ℕ+) < ofNat(n) ↔ OfNat.ofNat m < OfNat.ofNat n.

Русский

Для m,n ∈ ℕ с NeZero: (ofNat(m) : ℕ+) < ofNat(n) ↔ OfNat.ofNat m < OfNat.ofNat n.

LaTeX

$$$ (\\\\operatorname{ofNat}(m) : \\\\mathbb{N}^+) < \\\\operatorname{ofNat}(n) \\iff \\\\operatorname{OfNat.ofNat} m < \\\\operatorname{OfNat.ofNat} n. $$$

Lean4

@[simp]
theorem ofNat_lt_ofNat {m n : ℕ} [NeZero m] [NeZero n] : (ofNat(m) : ℕ+) < ofNat(n) ↔ OfNat.ofNat m < OfNat.ofNat n :=
  .rfl

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