ZerothHomotopy — Mathlib

English

ZerothHomotopy is the quotient of X by the pathSetoid, i.e., the space of path-connected components.

Русский

ZerothHomotopy — это фактор-пространство X по отношению эквивалентности по компонентам пути.

LaTeX

$$$ZerothHomotopy(X) = X / pathSetoid(X)$$$

Lean4

/-- The quotient type of points of a topological space modulo being joined by a continuous path. -/
def ZerothHomotopy :=
  Quotient (pathSetoid X)

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