continuous_of — Mathlib

English

A T1 space is equivalent to the statement that for all distinct x,y, the neighborhoods nhds x are disjoint from the pure filter at y (or equivalently that nhds x and pure y are disjoint).

Русский

T1-пространство эквивалентно тому, что для любых различных x,y окрестности x распадаются с чистыми фильтрами в y, то есть nhds x и pure y не пересекаются.

LaTeX

$$$T1Space(X) \\iff \\forall x \\forall y\\ (x \\neq y \\Rightarrow Disjoint(nhds(x), pure(y))).$$$

Lean4

theorem continuous_of [T1Space X] : Continuous (@CofiniteTopology.of X) :=
  t1Space_iff_continuous_cofinite_of.mp ‹_›

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