addNat_lt_addNat_iff — Mathlib

English

Let m be a natural number and i, j be elements of Fin n. Then i.addNat m < j.addNat m if and only if i < j.

Русский

Пусть m ∈ ℕ и i, j ∈ Fin(n). Тогда i.addNat m < j.addNat m тогда и только тогда, когда i < j.

LaTeX

$$$\forall {n : \mathbb{N}} (m : \mathbb{N}) {i j : \mathrm{Fin}(n)}, i.addNat m < j.addNat m \iff i < j$$$

Lean4

@[simp]
theorem addNat_lt_addNat_iff (m) {i j : Fin n} : i.addNat m < j.addNat m ↔ i < j :=
  (strictMono_addNat _).lt_iff_lt

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