Homotopy — Mathlib

English

The type of homotopies between two paths is the set of continuous maps from the square to X with boundary paths fixed.

Русский

Тип гомотопий между двумя путями — множество непрерывных отображений из квадрата в X с зафиксированными на границе путями.

LaTeX

$$$$\text{Homotopy}(p_0,p_1) := \{ F: I\times I \to X \mid F \text{ непрерывно}, F|_{\partial(I\times I)} = \text{boundary paths} \}.$$$$

Lean4

/-- The type of homotopies between two paths.
-/
abbrev Homotopy (p₀ p₁ : Path x₀ x₁) :=
  ContinuousMap.HomotopyRel p₀.toContinuousMap p₁.toContinuousMap {0, 1}

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