ConnectedComponents — Mathlib

English

The connected components form the quotient of a space by the relation x ∼ y ⇔ connectedComponent(x) = connectedComponent(y).

Русский

Связанные компоненты образуют факторпространство пространства по отношению x ∼ y, если компоненты x и y совпадают.

LaTeX

$$\mathrm{ConnectedComponents}(\alpha) = \operatorname{Quotient}\big(\{(x,y) \in \alpha\times\alpha \mid \operatorname{connectedComponent}(x) = \operatorname{connectedComponent}(y)\}\bigr).$$

Lean4

/-- The quotient of a space by its connected components -/
def ConnectedComponents (α : Type u) [TopologicalSpace α] :=
  Quotient (connectedComponentSetoid α)

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