natPred_le_natPred

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#PNat.natPred_le_natPred

English

For any m,n in ℕ+, m.natPred ≤ n.natPred iff m ≤ n.

Русский

Для любых m,n из ℕ+, m.natPred ≤ n.natPred эквивалентно m ≤ n.

LaTeX

$$$m,n \\in \\mathbb{N}_{>0} \\Rightarrow (m.natPred ≤ n.natPred) \\Leftrightarrow (m ≤ n).$$$

Lean4

@[simp]
theorem natPred_le_natPred {m n : ℕ+} : m.natPred ≤ n.natPred ↔ m ≤ n :=
  natPred_strictMono.le_iff_le

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

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

Разделы

Аффилиация

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