English
Let X be compact, Hausdorff, and totally disconnected. If x,y ∈ X satisfy Q.proj x = Q.proj y for every discrete quotient Q of X, then x = y. In other words, the family of projections separates points.
Русский
Пусть X компактное, Хазерфда и полностью несвязное. Если для любых дискретных quotients Q пространства X выполняется Q.proj x = Q.proj y, то x = y. То есть система проекций разделяет точки.
LaTeX
$$$\\forall x,y\\in X:\\; (\\forall Q: \\mathrm{DiscreteQuotient}\\,X,\\; Q.proj x = Q.proj y)\\;\\Rightarrow\\; x=y$ \nпри условии [T2Space X] [CompactSpace X] [disc : TotallyDisconnectedSpace X]$$
Lean4
theorem eq_of_forall_proj_eq [T2Space X] [CompactSpace X] [disc : TotallyDisconnectedSpace X] {x y : X}
(h : ∀ Q : DiscreteQuotient X, Q.proj x = Q.proj y) : x = y :=
by
rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_isClopen, mem_iInter]
rintro ⟨U, hU1, hU2⟩
exact (Quotient.exact' (h (ofIsClopen hU1))).mpr hU2
