cast_complex_isTheta_cast_real — Mathlib

English

The two natural embeddings Int → ℂ and Int → ℝ are Θ-equivalent with respect to the cofinite filter; i.e., their growth rates agree along cofinite subsets of ℕ.

Русский

Две вложения целых чисел в ℂ и ℝ равны по Θ-отношению относительно кофайн-фильтра; то есть их темпы роста совпадают на больших пространствах.

LaTeX

$$$ \\text{Int.cast}_{\\mathbb{C}} =_\\Theta^{cofinite} \\text{Int.cast}_{\\mathbb{R}} $$$

Lean4

theorem cast_complex_isTheta_cast_real : Int.cast (R := ℂ) =Θ[cofinite] Int.cast (R := ℝ) :=
  by
  apply Asymptotics.IsTheta.of_norm_eventuallyEq_norm
  filter_upwards with n using by simp

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