firstCountableTopology — Mathlib

English

Every pseudo-metrizable space is first countable.

Русский

Каждое псевдометризуемое пространство является пространством с первой счетной характеристикой.

LaTeX

$$$\text{FirstCountableTopology}(X)$ given $X$ pseudo-metrizable.$$

Lean4

/-- Every pseudo-metrizable space is first countable. -/
instance (priority := 100) firstCountableTopology [h : PseudoMetrizableSpace X] : FirstCountableTopology X :=
  by
  rcases h with ⟨_, hm⟩
  rw [← hm]
  exact
    @UniformSpace.firstCountableTopology X PseudoMetricSpace.toUniformSpace EMetric.instIsCountablyGeneratedUniformity

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