symm_bijective — Mathlib

English

The map Homotopy.symm is a bijection from Homotopy(p0,p1) to Homotopy(p1,p0), with inverse given by symm_symm.

Русский

Отображение Homotopy.symm образует биекцию между Homotopy(p0,p1) и Homotopy(p1,p0) с обратным отображением symm_symm.

LaTeX

$$$\forall p_0,p_1,\, (F : p_0.Homotopy p_1) \Rightarrow (\mathrm{Homotopy.symm}\, F) : p_1.Homotopy p_0$ и существует обратное.$$

Lean4

theorem symm_bijective : Function.Bijective (Homotopy.symm : Homotopy p₀ p₁ → Homotopy p₁ p₀) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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