cauchyFilter — Mathlib

English

If X has ultra-uniformity, then the CauchyFilter X also has ultra-uniformity.

Русский

Пусть X обладает ультра-равномерностью; тогда CauchyFilter X обладает ультра-равномерностью.

LaTeX

$$$IsUltraUniformity\big(\mathrm{CauchyFilter}(X)\big)$$$

Lean4

instance cauchyFilter [IsUltraUniformity X] : IsUltraUniformity (CauchyFilter X) :=
  by
  apply mk_of_hasBasis (CauchyFilter.basis_uniformity IsUltraUniformity.hasBasis)
  · exact fun _ ⟨_, hU, _⟩ ↦ hU.cauchyFilter_gen
  · exact fun _ ⟨_, _, hU⟩ ↦ hU.cauchyFilter_gen

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