uniformity_countably_generated — Mathlib

English

Let α be a group with a uniform structure. If the neighborhood filter at the identity is countably generated, then the uniformity on α is also countably generated.

Русский

Пусть α — группа с униформной структурой. Если фильтр окрестностей единицы порождается счётно, то и униформность на α порождается счётно.

LaTeX

$$$\\mathrm{IsCountablyGenerated}\\bigl((\\mathcal N (1:\\alpha))\\bigr) \\Rightarrow \\mathrm{IsCountablyGenerated}\\bigl(\\mathcal U(\\alpha)\\bigr)$$$

Lean4

@[to_additive]
theorem uniformity_countably_generated [(𝓝 (1 : α)).IsCountablyGenerated] : (𝓤 α).IsCountablyGenerated :=
  by
  rw [uniformity_eq_comap_nhds_one]
  exact Filter.comap.isCountablyGenerated _ _

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