exists_lb_coeff_ne — Mathlib

English

For any Laurent series x there exists f : RatFunc K with the same valuation as x.

Русский

Для любой LaurentSeries x существует f : RatFunc K с тем же значением в.

LaTeX

$$$\exists f : RatFunc K, Valued.v f = Valued.v x$$$

Lean4

theorem exists_lb_coeff_ne {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) : ∃ N, ∀ᶠ f : K⸨X⸩ in ℱ, ∀ d < N, coeff hℱ d = f.coeff d :=
  by
  obtain ⟨⟨N₁, hN₁⟩, ⟨N₂, hN₂⟩⟩ := exists_lb_eventual_support hℱ, exists_lb_support hℱ
  refine ⟨min N₁ N₂, ℱ.3 hN₁ fun _ hf d hd ↦ ?_⟩
  rw [hf d (lt_of_lt_of_le hd (min_le_left _ _)), hN₂ d (lt_of_lt_of_le hd (min_le_right _ _))]
    /- Given a Cauchy filter `ℱ` in the Laurent Series and a bound `D`, for almost all series in the
    filter the coefficients below `D` coincide with `Cauchy.coeff hℱ`. -/

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