not_infiniteNeg

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.InfinitePos.not_infiniteNeg

English

If x is InfinitePos, then x is not InfiniteNeg.

Русский

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

LaTeX

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

Lean4

theorem not_infiniteNeg {x : ℝ*} (hp : InfinitePos x) : ¬InfiniteNeg x := fun hn ↦ hn.not_infinitePos hp

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

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

Разделы

Аффилиация

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