symm — Mathlib

English

If F is a homotopy from p0 to p1, then F.symm is a homotopy from p1 to p0.

Русский

Если F — гомотопия между p0 и p1, то F.symm является гомотопией между p1 и p0.

LaTeX

$$$\forall X\, [TopologicalSpace X], \forall p_0,p_1 : Path\, x_0 x_1, (F : p_0.Homotopy p_1) \Rightarrow F.symm : p_1.Homotopy p_0$$$

Lean4

/-- Given a `Homotopy p₀ p₁`, we can define a `Homotopy p₁ p₀` by reversing the homotopy.
-/
@[simps!]
def symm (F : Homotopy p₀ p₁) : Homotopy p₁ p₀ :=
  ContinuousMap.HomotopyRel.symm F

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