instInhabitedHomotopyGroup — Mathlib

English

The nth homotopy group for a finite index n is the same as the homotopy group with N = Fin n.

Русский

n-ая гомотопия группы для конечного индекса n эквивалентна гомотопии группе с N = Fin n.

LaTeX

$$$\\mathrm{HomotopyGroup.Pi}(n,X,x) := \\mathrm{HomotopyGroup}(\\mathrm{Fin}(n),X,x)$$$

Lean4

instance : Inhabited (HomotopyGroup N X x) :=
  inferInstanceAs <| Inhabited <| Quotient (GenLoop.Homotopic.setoid N x)

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