tendsto_const_mul_pow_atTop_iff — Mathlib

English

For a fixed c and n, Tendsto (c · x^n) atTop atTop holds iff n ≠ 0 and c > 0.

Русский

Для фиксированных c и n, Tendsto (c · x^n) к бесконечности равно atTop тогда и только тогда, когда n ≠ 0 и c > 0.

LaTeX

$$$\operatorname{Tendsto}(x \mapsto c \cdot x^{n})\text{ atTop} \text{ atTop} \iff (n \neq 0) \land (0 < c)$$$

Lean4

theorem tendsto_const_mul_pow_atTop_iff : Tendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c :=
  by
  refine ⟨fun h => ⟨?_, ?_⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩
  · rintro rfl
    simp only [pow_zero, not_tendsto_const_atTop] at h
  · rcases ((h.eventually_gt_atTop 0).and (eventually_ge_atTop 0)).exists with ⟨k, hck, hk⟩
    exact pos_of_mul_pos_left hck (pow_nonneg hk _)

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