LoopSpace — Mathlib

English

GenLoop(N,X,x) is the set of continuous maps p: I^N → X that send every boundary point of the cube to x.

Русский

GenLoop(N,X,x) — множество непрерывных отображений I^N → X, таких что на границе куба все точки идут в x.

LaTeX

$$GenLoop(N, X, x) = { p ∈ C(I^N, X) | ∀ y ∈ Cube.boundary N, p(y) = x }$$

Lean4

/-- The space of paths with both endpoints equal to a specified point `x : X`.
Denoted as `Ω`, within the `Topology.Homotopy` namespace. -/
abbrev LoopSpace :=
  Path x x

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