notMem_range_self

Mathlib.Data.Multiset.Range

URI: https://scilib.ai/kg/mathlib#Multiset.notMem_range_self

English

n is not an element of range n.

Русский

n не является элементом range n.

LaTeX

$$$n \notin \mathrm{range}(n)$$$

Lean4

theorem notMem_range_self {n : ℕ} : n ∉ range n :=
  List.not_mem_range_self

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

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

Разделы

Аффилиация

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