not_infinitePos

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.InfiniteNeg.not_infinitePos

English

If x is InfiniteNeg, then x is not InfinitePos.

Русский

Если x бесконечно отрицательно, то x не бесконечно положительно.

LaTeX

$$$\forall {x}, \; \mathrm{InfiniteNeg}(x) \rightarrow \lnot \mathrm{InfinitePos}(x)$$$

Lean4

theorem not_infinitePos {x : ℝ*} : InfiniteNeg x → ¬InfinitePos x := fun hn hp => (hn 0).not_gt (hp 0)

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

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

Разделы

Аффилиация

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