eq — Mathlib · SciLib

English

In a T0 space, a set S has at most one generic point; if two generic points x,y exist for S, then x = y.

Русский

В пространстве T0 множество S имеет не более одной обобщенной точки; если две существующие обобщенные точки x и y для S, то x = y.

LaTeX

$$$ \text{[T0 Space]} \rightarrow (\mathrm{IsGenericPoint}(x,S) \land \mathrm{IsGenericPoint}(y,S) \rightarrow x = y)$$$

Lean4

/-- In a T₀ space, each set has at most one generic point. -/
protected theorem eq [T0Space α] (h : IsGenericPoint x S) (h' : IsGenericPoint y S) : x = y :=
  (h.inseparable h').eq

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