coe_lt_coe — Mathlib

English

For natural numbers, the strict order is preserved under casting: (x : PartENat) < y ↔ x < y.

Русский

Для натуральных чисел строгое неравенство сохраняется при приведении к PartENat: (x : PartENat) < y ↔ x < y.

LaTeX

$$$ (x : \mathrm{PartENat}) < y \iff x < y $$$

Lean4

/-- Alias of `Nat.cast_lt` specialized to `PartENat` -/
theorem coe_lt_coe {x y : ℕ} : (x : PartENat) < y ↔ x < y :=
  Nat.cast_lt

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