cauchy_nhds

Mathlib.Topology.UniformSpace.Cauchy

URI: https://scilib.ai/kg/mathlib#cauchy_nhds

English

For any a in α, the neighborhood filter nhds a is Cauchy.

Русский

Для любого a ∈ α фильтр окрестностей nhds a является Коши.

LaTeX

$$$ \forall a:\alpha,\; \text{Cauchy}(\nhds a)$$$

Lean4

theorem cauchy_nhds {a : α} : Cauchy (𝓝 a) :=
  ⟨nhds_neBot, nhds_prod_eq.symm.trans_le (nhds_le_uniformity a)⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru