shiftLeft_lt

Mathlib.Data.Nat.Bitwise

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

← MathLib Explorer

English

If x < 2^n, then x shifted left by m positions is strictly less than 2^{n+m}.

Русский

Если x < 2^n, то x сдвинутое влево на m позиций менее чем 2^{n+m}.

LaTeX

$$$ x \cdot 2^{m} < 2^{n+m} \quad\text{при } x < 2^{n} $$$

Lean4

theorem shiftLeft_lt {x n m : ℕ} (h : x < 2 ^ n) : x <<< m < 2 ^ (n + m) := by
  simp only [Nat.pow_add, shiftLeft_eq, Nat.mul_lt_mul_right (Nat.two_pow_pos _), h]

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

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

Разделы

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

Аффилиация

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