cauchyFilter_iff — Mathlib

English

IsUltraUniformity(CauchyFilter X) is equivalent to IsUltraUniformity X.

Русский

Ультраравномерность фильтра Коши эквивалентна ультра-равномерности самого пространства.

LaTeX

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

Lean4

@[simp]
theorem cauchyFilter_iff : IsUltraUniformity (CauchyFilter X) ↔ IsUltraUniformity X :=
  ⟨fun _ ↦ CauchyFilter.isUniformInducing_pureCauchy.isUltraUniformity, fun _ ↦ inferInstance⟩

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