not_infinite_real

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.not_infinite_real

← MathLib Explorer

English

All real numbers are not infinite.

Русский

Каждое вещественное число не бесконечно.

LaTeX

$$$\\forall r \\in \\mathbb{R}, \\neg Infinite(r)$$$

Lean4

theorem not_infinite_real (r : ℝ) : ¬Infinite r :=
  by
  rw [not_infinite_iff_exist_lt_gt]
  exact ⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩

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

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

Разделы

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

Аффилиация

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