to_sequentialSpace — Mathlib

English

Every Frechet-Urysohn space is a sequential space.

Русский

Каждое пространство Фреше–Ури́шхо́н является последовательным пространством.

LaTeX

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

Lean4

/-- Every Fréchet-Urysohn space is a sequential space. -/
instance (priority := 100) to_sequentialSpace [FrechetUrysohnSpace X] : SequentialSpace X :=
  ⟨fun s hs => by rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]⟩

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