eq_pure_cauchyConst — Mathlib

English

In a discrete uniform space, every Cauchy filter is equal to the pure filter at a constant point determined by cauchyConst.

Русский

В дискретном равномерном пространстве каждый Cauchy-фильтр равен чистому фильтру в константной точке, определяемой cauchyConst.

LaTeX

$$$f = pure (cauchyConst\\ f)$$$

Lean4

theorem eq_pure_cauchyConst {f : Filter α} (hf : Cauchy f) : f = pure (cauchyConst hf) :=
  (eq_pure_of_cauchy hf).choose_spec

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