infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg

English

If x is InfiniteNeg and y is not infinitesimal with y > 0, then (x*y) is InfiniteNeg.

Русский

Если x бесконечно велико отрицательно и y > 0 не инфинитезимально, то x·y бесконечно отрицательно.

LaTeX

$$$\operatorname{InfiniteNeg}(x) \land \lnot \operatorname{Infinitesimal}(y) \land 0 < y \Rightarrow \operatorname{InfiniteNeg}(x y)$$$

Lean4

theorem infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg {x y : ℝ*} :
    ¬Infinitesimal x → x < 0 → InfiniteNeg y → InfinitePos (x * y) := fun hx hp hy =>
  mul_comm y x ▸ infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg hy hx hp

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