infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg

English

If x ≠ Infinitesimal and x < 0 and y is InfiniteNeg, then x*y is InfiniteNeg.

Русский

Если x неInfinitesimal и x < 0 и y InfiniteNeg, то x*y InfiniteNeg.

LaTeX

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

Lean4

theorem infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg {x y : ℝ*} :
    ¬Infinitesimal x → 0 < x → InfiniteNeg y → InfiniteNeg (x * y) := fun hx hp hy => by rw [mul_comm];
  exact infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp

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