pi1EquivFundamentalGroup — Mathlib

English

The first homotopy group at x is in bijection with the fundamental group of X at x.

Русский

Первая гомотопия группы в x биекция с фундаментальной группой X в x.

LaTeX

$$$\\mathrm{pi1EquivFundamentalGroup}: \\pi_1 X x \\simeq \\pi_1(X,x)$$$

Lean4

/-- The first homotopy group at `x` is in bijection with the fundamental group. -/
def pi1EquivFundamentalGroup : π_ 1 X x ≃ FundamentalGroup X x :=
  homotopyGroupEquivFundamentalGroupOfUnique (Fin 1)

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