JoinedIn — Mathlib

English

The quotient type of points of a topological space modulo being joined by a continuous path.

Русский

Тип фактор по отношению «соединено путём» для пространства.

LaTeX

$$$ZerothHomotopy = Quotient (pathSetoid X)$$$

Lean4

/-- The relation "being joined by a path in `F`". Not quite an equivalence relation since it's not
reflexive for points that do not belong to `F`. -/
def JoinedIn (F : Set X) (x y : X) : Prop :=
  ∃ γ : Path x y, ∀ t, γ t ∈ F

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