instInfiniteNat

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#instInfiniteNat

← MathLib Explorer

English

The natural numbers N are infinite.

Русский

Натуральные числа N бесконечны.

LaTeX

$$$\\operatorname{Infinite}(\\mathbb{N})$$$

Lean4

instance : Infinite ℕ :=
  Infinite.of_not_fintype <| by
    intro h
    exact (Finset.range _).card_le_univ.not_gt ((Nat.lt_succ_self _).trans_eq (card_range _).symm)

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

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

Разделы

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

Аффилиация

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