English
The range of the coefficient-to-Laurent-series embedding is dense in the codomain, i.e., rational Laurent series are dense in Laurent series.
Русский
Область отображения коэффициентов в лаурентовые ряды плотна в cadomain; рациональные лаурентные ряды плотно внутри лаурентных.
LaTeX
$$$\text{DenseRange}( (\uparrow) : RatFunc K → K⸨X⸩ )$$$
Lean4
theorem coe_range_dense : DenseRange ((↑) : RatFunc K → K⸨X⸩) :=
by
rw [denseRange_iff_closure_range]
ext f
simp only [UniformSpace.mem_closure_iff_symm_ball, Set.mem_univ, iff_true, Set.Nonempty, Set.mem_inter_iff,
Set.mem_range, exists_exists_eq_and]
intro V hV h_symm
rw [uniformity_eq_comap_neg_add_nhds_zero_swapped] at hV
obtain ⟨T, hT₀, hT₁⟩ := hV
obtain ⟨γ, hγ⟩ := Valued.mem_nhds_zero.mp hT₀
obtain ⟨P, _⟩ := exists_ratFunc_val_lt f γ
use P
apply hT₁
apply hγ
simpa only [add_comm, ← sub_eq_add_neg, gt_iff_lt, Set.mem_setOf_eq]
