firstCountableTopology — Mathlib

English

A uniform space with a countable generated uniformity has a first-countable topology.

Русский

Уравномерное пространство с порожденной счетной базой имеет топологию с первой счётной базой.

LaTeX

$$$\text{FirstCountableTopology}(\alpha)$$$

Lean4

instance (priority := 100) firstCountableTopology : FirstCountableTopology α :=
  ⟨fun a => by rw [nhds_eq_comap_uniformity]; infer_instance⟩

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