English
For any F in a polynomial power series context and any valuation bound η, there exists a polynomial P with intValuation(F−P) < η.
Русский
Для любого F и ограничителя валюирования η существует многочлен P такой, что intValuation(F−P) < η.
LaTeX
$$$\exists P : K[X], (PowerSeries.idealX K).intValuation (F - P) < η$$$
Lean4
/-- Since extracting coefficients is uniformly continuous, every Cauchy filter in
`K⸨X⸩` gives rise to a Cauchy filter in `K` for every `d : ℤ`, and such Cauchy filter
in `K` converges to a principal filter -/
def coeff {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) : ℤ → K :=
let _ : UniformSpace K := ⊥
fun d ↦ DiscreteUniformity.cauchyConst <| hℱ.map (uniformContinuous_coeff d)
