infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos

English

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

Русский

Если x InfiniteNeg и y > 0 не инфинитезимально, то x·y InfiniteNeg.

LaTeX

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

Lean4

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

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