lt_size_self — Mathlib

English

For every n ∈ ℕ, n < 2^{size n}.

Русский

Для каждого n ∈ ℕ выполняется n < 2^{size(n)}.

LaTeX

$$$n < 2^{\operatorname{size}(n)}$$$

Lean4

theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
  rw [← one_shiftLeft]
  have : ∀ {n}, n = 0 → n < 1 <<< (size n) := by simp
  refine binaryRec ?_ ?_ n
  · apply this rfl
  intro b n IH
  by_cases h : bit b n = 0
  · apply this h
  rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul]
  cases b <;> dsimp [bit] <;> omega

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