size_pow

Mathlib.Data.Nat.Size

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

← MathLib Explorer

English

For all n ∈ ℕ, size(2^n) = n + 1.

Русский

Для всех n ∈ ℕ размер(2^n) равен n + 1.

LaTeX

$$$\operatorname{size}(2^{n}) = n + 1$$$

Lean4

theorem size_pow {n : ℕ} : size (2 ^ n) = n + 1 :=
  le_antisymm (size_le.2 <| Nat.pow_lt_pow_right (by decide) (lt_succ_self _)) (lt_size.2 <| le_rfl)

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

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

Разделы

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

Аффилиация

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