tendsto_atBot_iff_leadingCoeff_nonpos

English

The limit towards atTop equals atBot iff the leading coefficient is nonpositive with negative degree.

Русский

Предел при стремлении к бесконечности равен минус бесконечности тогда и только тогда, когда ведущий коэффициент не положителен и степень положительна.

LaTeX

$$$$\text{Tendsto atTop to atBot} \iff 0 < \deg(P) \land P.leadingCoeff \le 0.$$$$

Lean4

theorem tendsto_atBot_iff_leadingCoeff_nonpos :
    Tendsto (fun x => eval x P) atTop atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0 := by
  simp only [← tendsto_neg_atTop_iff, ← eval_neg, tendsto_atTop_iff_leadingCoeff_nonneg, degree_neg, leadingCoeff_neg,
    neg_nonneg]

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