ofNat_le_ofNat

Mathlib.Data.Bool.Basic

URI: https://scilib.ai/kg/mathlib#Bool.ofNat_le_ofNat

← MathLib Explorer

English

If n ≤ m then ofNat(n) ≤ ofNat(m).

Русский

Если n ≤ m, то ofNat(n) ≤ ofNat(m).

LaTeX

$$$ \forall {n,m : \mathbb{N}},\; n \le m \rightarrow \text{ofNat}(n) \le \text{ofNat}(m) $$$

Lean4

theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m :=
  by
  simp only [ofNat, ne_eq, _root_.decide_not]
  cases Nat.decEq n 0 with
  | isTrue hn => grind [Bool.false_le]
  | isFalse hn => cases Nat.decEq m 0 with grind [Bool.le_true]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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