HomotopyGroup — Mathlib

English

The nth homotopy group at x is defined as the quotient of GenLoop.Homotopic setoid N x by the GenLoop homotopy relation.

Русский

n-ая гомотопия группы в точке x определяется как факторгруппа по отношению GenLoop.Homotopic (множество N x).

LaTeX

$$$\\mathrm{HomotopyGroup}(N,X,x) := \\operatorname{Quotient}(\\mathrm{GenLoop.Homotopic.setoid}\\, N\\, x)$$$

Lean4

/-- The `n`th homotopy group at `x` defined as the quotient of `Ω^n x` by the
  `GenLoop.Homotopic` relation. -/
def HomotopyGroup (N X : Type*) [TopologicalSpace X] (x : X) : Type _ :=
  Quotient (GenLoop.Homotopic.setoid N x)

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