symm — Mathlib

English

For any f0,f1: C(X,Y), there is a reverse homotopy from f1 back to f0, defined by (F.symm)(t,x) = F(σ t, x) where σ is t ↦ 1−t.

Русский

Существует обратная гомотопия от f1 к f0, определяемая (F.symm)(t,x)=F(1−t,x).

LaTeX

$$$F\text{.symm}(t,x)=F(\sigma t, x) = F(1-t, x)$$$

Lean4

/-- Given a `Homotopy f₀ f₁`, we can define a `Homotopy f₁ f₀` by reversing the homotopy.
-/
@[simps]
def symm {f₀ f₁ : C(X, Y)} (F : Homotopy f₀ f₁) : Homotopy f₁ f₀
    where
  toFun x := F (σ x.1, x.2)
  map_zero_left := by simp
  map_one_left := by norm_num

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