infinite_setOf_prime

Mathlib.Data.Nat.PrimeFin

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

← MathLib Explorer

English

The set of primes is infinite.

Русский

Множество простых чисел бесконечно.

LaTeX

$$$\{p \in \mathbb{N} \mid \operatorname{Prime}(p)\} \text{ is infinite}$$$

Lean4

/-- A version of `Nat.exists_infinite_primes` using the `Set.Infinite` predicate. -/
theorem infinite_setOf_prime : {p | Prime p}.Infinite :=
  Set.infinite_of_not_bddAbove not_bddAbove_setOf_prime

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

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

Разделы

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

Аффилиация

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