infinitePos_mul_of_infinitePos_not_infinitesimal_pos

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_infinitePos_not_infinitesimal_pos {x y : ℝ*} :
    InfinitePos x → ¬Infinitesimal y → 0 < y → InfinitePos (x * y) := fun hx hy₁ hy₂ r =>
  by
  have hy₁' := not_forall.mp (mt infinitesimal_def.2 hy₁)
  let ⟨r₁, hy₁''⟩ := hy₁'
  have hyr : 0 < r₁ ∧ ↑r₁ ≤ y := by rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
  rw [← div_mul_cancel₀ r (ne_of_gt hyr.1), coe_mul]
  exact mul_lt_mul (hx (r / r₁)) hyr.2 (coe_lt_coe.2 hyr.1) (le_of_lt (hx 0))

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