ne_real

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.Infinite.ne_real

English

If x is infinite, then x ≠ r for every real r.

Русский

Если x бесконечно велик, то x не равно никакому вещественному числу.

LaTeX

$$$\\forall x \\in \\mathbb{R}^*, \\ Infinite(x) \\rightarrow \\forall r \\in \\mathbb{R}, x \\neq r$$$

Lean4

theorem ne_real {x : ℝ*} : Infinite x → ∀ r : ℝ, x ≠ r := fun hi r hr =>
  not_infinite_real r <| @Eq.subst _ Infinite _ _ hr hi

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

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

Разделы

Аффилиация

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