frechetUrysohnSpace — Mathlib

English

Every space with a first-countable topology is Frechet-Urysohn.

Русский

Любое пространство с топологией первого счётчика является пространством Фреше–Ури́шхо́н.

LaTeX

$$$\text{FirstCountableTopology}(X) \Rightarrow \text{FrechetUrysohnSpace}(X)$$$

Lean4

/-- Every first-countable space is a Fréchet-Urysohn space. -/
instance (priority := 100) frechetUrysohnSpace [FirstCountableTopology X] : FrechetUrysohnSpace X :=
  FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto fun _ _ =>
    tendsto_iff_seq_tendsto.2
      -- see Note [lower instance priority]

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