notMem_bitIndices_self

Mathlib.Data.Nat.BitIndices

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

English

For every natural number n, n is not an element of its bitIndices.

Русский

Для каждого натурального числа n, n не принадлежит его битовым индексам.

LaTeX

$$$\forall n \\in \mathbb{N}, \ n \notin n.\mathrm{bitIndices}$$$

Lean4

theorem notMem_bitIndices_self (n : ℕ) : n ∉ n.bitIndices := fun h ↦
  (n.lt_two_pow_self).not_ge <| two_pow_le_of_mem_bitIndices h

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

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

Разделы

Аффилиация

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