infinitePos_omega

Mathlib.Analysis.Real.Hyperreal

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

English

The special hyperreal ω is infinitely large (InfinitePos).

Русский

Особая гиперреальная величина ω бесконечно велика (InfinitePos).

LaTeX

$$$\operatorname{InfinitePos}(\omega)$$$

Lean4

theorem infinitePos_omega : InfinitePos ω :=
  infinitePos_iff_infinitesimal_inv_pos.mpr ⟨infinitesimal_epsilon, epsilon_pos⟩

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

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

Разделы

Аффилиация

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