toNat_le_toNat

Mathlib.Data.Bool.Basic

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

English

If b0 ≤ b1 then toNat(b0) ≤ toNat(b1).

Русский

Если b0 ≤ b1, то toNat(b0) ≤ toNat(b1).

LaTeX

$$$ \forall {b_0 b_1 : Bool},\; b_0 \le b_1 \rightarrow toNat(b_0) \le toNat(b_1) $$$

Lean4

theorem toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁ := by
  cases b₀ <;> cases b₁ <;> simp_all +decide

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

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

Разделы

Аффилиация

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