natAdd_le_natAdd_iff — Mathlib

English

For any m, i,j ∈ Fin(n), natAdd m i ≤ natAdd m j iff i ≤ j.

Русский

Для любого m, i,j ∈ Fin(n) выполняется natAdd m i ≤ natAdd m j тогда и только тогда, когда i ≤ j.

LaTeX

$$$\forall {n:\mathbb{N}} (m:\mathbb{N})\; {i,j:\mathrm{Fin}(n)},\; \mathrm{natAdd}(m,i) \le \mathrm{natAdd}(m,j) \iff i \le j$$$

Lean4

@[simp]
theorem natAdd_le_natAdd_iff (m) {i j : Fin n} : natAdd m i ≤ natAdd m j ↔ i ≤ j :=
  (strictMono_natAdd _).le_iff_le

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