symm_bijective — Mathlib

English

The map Homotopy.symm: Homotopy f0 f1 → Homotopy f1 f0 is bijective with inverse itself.

Русский

Отображение Homotopy.symm: Homotopy f0 f1 → Homotopy f1 f0 биективно и имеет обратную саму по себе.

LaTeX

$$Function.Bijective (Homotopy.symm)$$

Lean4

theorem symm_bijective {f₀ f₁ : C(X, Y)} : Function.Bijective (Homotopy.symm : Homotopy f₀ f₁ → Homotopy f₁ f₀) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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