instRegularSpace — Mathlib

English

Every completely regular space is a regular space.

Русский

Каждое полностью регулярное пространство является регулярным.

LaTeX

$$$\\text{CompletelyRegularSpace }X \\rightarrow \\text{RegularSpace }X$$$

Lean4

instance instRegularSpace [CompletelyRegularSpace X] : RegularSpace X :=
  by
  rw [regularSpace_iff]
  intro s a hs ha
  obtain ⟨f, cf, hf, hhf⟩ := CompletelyRegularSpace.completely_regular a s hs ha
  apply disjoint_of_map (f := f)
  apply Disjoint.mono (cf.tendsto_nhdsSet_nhds hhf) cf.continuousAt
  exact disjoint_nhds_nhds.mpr (hf.symm ▸ zero_ne_one).symm

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