cauchy_pure

Mathlib.Topology.UniformSpace.Cauchy

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

English

For any a in α, the pure filter at a, pure a, is Cauchy.

Русский

Пусть для любого a ∈ α фильтр чисто-условный (pure a) является Коши.

LaTeX

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

Lean4

theorem cauchy_pure {a : α} : Cauchy (pure a) :=
  cauchy_nhds.mono (pure_le_nhds a)

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

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

Разделы

Аффилиация

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