delayReflLeft — Mathlib

English

DelayReflLeft θ γ is defined as the reverse of delayReflRight θ applied to γ.symm.

Русский

DelayReflLeft θ γ задан как обратный к delayReflRight θ примененный к γ.symm.

LaTeX

$$delayReflLeft(θ, γ) := (delayReflRight(θ, γ.symm)).symm$$

Lean4

/-- This is the function on p. 475 of [serre1951], defining a homotopy from a path `γ` to the
product path `e ∧ γ`. -/
def delayReflLeft (θ : I) (γ : Path x y) : Path x y :=
  (delayReflRight θ γ.symm).symm

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