bit_lt_bit

Mathlib.Data.Nat.Bits

URI: https://scilib.ai/kg/mathlib#Nat.bit_lt_bit

← MathLib Explorer

English

If m < n, then bit a m < bit b n for any a,b ∈ {true,false}.

Русский

Если m < n, то bit a m < bit b n для любых a,b ∈ {true,false}.

LaTeX

$$$$ \forall (a,b : \mathrm{Bool}) (h : m < n), \; \text{bit}(a,m) < \text{bit}(b,n). $$$$

Lean4

theorem bit_lt_bit (a b) (h : m < n) : bit a m < bit b n :=
  calc
    bit a m < 2 * n := by cases a <;> dsimp [bit] <;> omega
    _ ≤ bit b n := by cases b <;> dsimp [bit] <;> omega

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

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

Разделы

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

Аффилиация

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