infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg

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_infiniteNeg_not_infinitesimal_neg {x y : ℝ*} :
    InfiniteNeg x → ¬Infinitesimal y → y < 0 → InfinitePos (x * y) :=
  by
  rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]
  exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

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