fundamentalGroupMulEquivOfPath — Mathlib

English

Given a path p from x0 to x1, there is a MulEquiv between FundamentalGroup X x0 and FundamentalGroup X x1.

Русский

Дана последовательность p между точками, существует MulEquiv между FundamentalGroup(X,x0) и FundamentalGroup(X,x1).

LaTeX

$$$$ \\operatorname{FundamentalGroup}(X,x_0) \\cong_* \\operatorname{FundamentalGroup}(X,x_1). $$$$

Lean4

/-- Get an isomorphism between the fundamental groups at two points given a path -/
def fundamentalGroupMulEquivOfPath (p : Path x₀ x₁) : FundamentalGroup X x₀ ≃* FundamentalGroup X x₁ :=
  Aut.autMulEquivOfIso (asIso ⟦p⟧)

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