infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos

English

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

Русский

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

LaTeX

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

Lean4

theorem infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos {x y : ℝ*} :
    InfiniteNeg x → ¬Infinitesimal y → 0 < y → InfiniteNeg (x * y) :=
  by
  rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]
  exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

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