instR0Space — Mathlib

English

In any topological space X with R1Space, we have R0Space X; i.e., every R1-space is R0.

Русский

В любой топологической пространстве X с R1Space выполняется R0Space, то есть каждое R1-пространство является R0.

LaTeX

$$$ \\forall X\\ [TopologicalSpace X] [R1Space X],\\; R0Space X. $$$

Lean4

instance (priority := 100) : R0Space X where
  specializes_symmetric _ _ h := (specializes_or_disjoint_nhds _ _).resolve_right <| fun hd ↦ h.not_disjoint hd.symm

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