addNat_le_addNat_iff

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.addNat_le_addNat_iff

English

For any m, i.addNat m ≤ j.addNat m iff i ≤ j.

Русский

Для любого m: i.addNat m ≤ j.addNat m эквивалентно i ≤ j.

LaTeX

$$$\forall m:\ \mathrm{Fin}(n)\; i,j:\ i.addNat(m) \le j.addNat(m) \iff i \le j.$$$

Lean4

@[simp]
theorem addNat_le_addNat_iff (m) {i j : Fin n} : i.addNat m ≤ j.addNat m ↔ i ≤ j :=
  (strictMono_addNat _).le_iff_le

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru