infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg

English

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

Русский

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

LaTeX

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

Lean4

theorem infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg {x y : ℝ*} :
    InfinitePos x → ¬Infinitesimal y → y < 0 → InfiniteNeg (x * y) :=
  by
  rw [← infinitePos_neg, ← neg_pos, neg_mul_eq_mul_neg, ← infinitesimal_neg]
  exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

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