injective_stoneCechUnit_of_t35Space

English

If X is a T35 space, the canonical map stoneCechUnit: X → StoneCech X is injective.

Русский

Пусть X является пространством класса T35. Каноническое отображение stoneCechUnit: X → StoneCech X инъективно.

LaTeX

$$$\forall a,b\in X,\ stoneCechUnit(a)=stoneCechUnit(b)\Rightarrow a=b$$$

Lean4

theorem injective_stoneCechUnit_of_t35Space [T35Space X] : Function.Injective (stoneCechUnit : X → StoneCech X) :=
  by
  intro a b hab
  contrapose hab
  obtain ⟨f, fc, fab⟩ := separatesPoints_continuous_of_t35Space_Icc hab
  exact fun q ↦ fab (eq_if_stoneCechUnit_eq fc q)

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