size_bit

Mathlib.Data.Nat.Size

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

← MathLib Explorer

English

If bit b n ≠ 0, then size(bit b n) = succ(size n).

Русский

Если бит b n ≠ 0, то размер bit b n равен succ (размер n).

LaTeX

$$$ \\text{size}(\\text{bit } b\, n) = \\operatorname{succ}(\\text{size}(n)) $$$

Lean4

@[simp]
theorem size_bit {b n} (h : bit b n ≠ 0) : size (bit b n) = succ (size n) :=
  by
  unfold size
  conv =>
    lhs
    rw [binaryRec]
    simp [h]

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

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

Разделы

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

Аффилиация

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