fromPath — Mathlib

English

Convert a path in a space to an arrow in the fundamental groupoid.

Русский

Пусть путь в пространстве преобразуется в стрелку в фундаментальном групоидe.

LaTeX

$$$$ \\text{fromPath}: \\text{Path.Homotopic.Quotient}(x_0,x_1) \\to \\mathrm{Hom}_{\\mathrm{FundamentalGroupoid}(X)}(x_0,x_1). $$$$

Lean4

/-- Help the typechecker by converting a path in a topological space to an arrow in the
fundamental groupoid of that space. -/
abbrev fromPath {X : TopCat} {x₀ x₁ : X} (p : Path.Homotopic.Quotient x₀ x₁) :
    FundamentalGroupoid.mk x₀ ⟶ FundamentalGroupoid.mk x₁ :=
  p

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