symm — Mathlib

English

Reversing the direction of a homotopy yields a HomotopyWith f1 f0 P.

Русский

Обратное направление гомотопии даёт HomotopyWith f1 f0 P.

LaTeX

$$$\\text{symm}: HomotopyWith(f_0,f_1,P) \\to HomotopyWith(f_1,f_0,P)$$$

Lean4

/-- Given a `HomotopyWith f₀ f₁ P`, we can define a `HomotopyWith f₁ f₀ P` by reversing the homotopy.
-/
@[simps!]
def symm {f₀ f₁ : C(X, Y)} (F : HomotopyWith f₀ f₁ P) : HomotopyWith f₁ f₀ P
    where
  toHomotopy := F.toHomotopy.symm
  prop' := fun t => F.prop (σ t)

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