trans — Mathlib

English

If F is a homotopy from p0 to p1 and G is a homotopy from p1 to p2, then F.trans G is a homotopy from p0 to p2.

Русский

Если F — гомотопия от p0 к p1, а G — от p1 к p2, то F.trans G — гомотопия от p0 к p2.

LaTeX

$$$\forall F : p_0.Homotopy p_1,\; \forall G : p_1.Homotopy p_2,\; (F.trans G) : p_0.Homotopy p_2$$$

Lean4

/-- Given `Homotopy p₀ p₁` and `Homotopy p₁ p₂`, we can define a `Homotopy p₀ p₂` by putting the first
homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
-/
def trans (F : Homotopy p₀ p₁) (G : Homotopy p₁ p₂) : Homotopy p₀ p₂ :=
  ContinuousMap.HomotopyRel.trans F G

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