instIsCountablyGeneratedUniformity

Mathlib.Topology.EMetricSpace.Defs

URI: https://scilib.ai/kg/mathlib#EMetric.instIsCountablyGeneratedUniformity

← MathLib Explorer

English

The uniformity 𝓤 α is countably generated.

Русский

Униформность 𝓤 α счетно порождаема.

LaTeX

$$$ 𝓤(\alpha) \text{ is countably generated. }$$$

Lean4

instance (priority := 900) instIsCountablyGeneratedUniformity : IsCountablyGenerated (𝓤 α) :=
  isCountablyGenerated_of_seq ⟨_, uniformity_basis_edist_inv_nat.eq_iInf⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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