coe_le_coe — Mathlib

English

Casting natural numbers into PartENat preserves the order: for all x,y ∈ ℕ, (x : PartENat) ≤ y ↔ x ≤ y.

Русский

Преобразование натуральных чисел в PartENat сохраняет порядок: для всех x,y ∈ ℕ, (x : PartENat) ≤ y ↔ x ≤ y.

LaTeX

$$$ \forall x,y : \mathbb{N}, \ (x : \mathrm{PartENat}) \le y \iff x \le y $$$

Lean4

/-- Alias of `Nat.cast_le` specialized to `PartENat` -/
theorem coe_le_coe {x y : ℕ} : (x : PartENat) ≤ y ↔ x ≤ y :=
  Nat.cast_le

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