instLaurentSeriesComplete — Mathlib

English

Given a Cauchy LaurentSeries filter, every neighborhood of its limit contains almost all series in the filter.

Русский

Для фильтра серии Лаурента Cauchy любая окрестность предела содержит почти все элементы фильтра.

LaTeX

$$$\forall{K} [\text{Field } K], \text{...} \Rightarrow \forall \mathcal F, \text{nhds}(\text{Cauchy.limit } \mathcal F) \ni U \Rightarrow \forall f \in \mathcal F, f \in U$$$

Lean4

instance instLaurentSeriesComplete : CompleteSpace K⸨X⸩ :=
  ⟨fun hℱ ↦ ⟨Cauchy.limit hℱ, fun _ hS ↦ Cauchy.eventually_mem_nhds hℱ hS⟩⟩

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