infinitePos_mul_of_not_infinitesimal_pos_infinitePos

English

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

Русский

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

LaTeX

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

Lean4

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

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