natAdd_lt_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) < \mathrm{natAdd}(m,j) \iff i < j$$$

Lean4

@[simp]
theorem natAdd_lt_natAdd_iff (m) {i j : Fin n} : natAdd m i < natAdd m j ↔ i < j :=
  (strictMono_natAdd _).lt_iff_lt

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