natCast_covBy — Mathlib

English

Natural embedding preserves the cover relation: for a,b ∈ ℕ, (a:ℤ) ⋖ b iff a ⋖ b.

Русский

Естественное вложение сохраняет отношение покрытия: для a,b ∈ ℕ, (a:ℤ) ⋖ b эквивалентно a ⋖ b.

LaTeX

$$$(a : \mathbb{Z}) \prec b \iff a \prec b$$$

Lean4

@[simp, norm_cast]
theorem natCast_covBy {a b : ℕ} : (a : ℤ) ⋖ b ↔ a ⋖ b :=
  by
  rw [Order.covBy_iff_add_one_eq, Order.covBy_iff_add_one_eq]
  exact Int.natCast_inj

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