symm_bijective — Mathlib

English

The map Symm is bijective between HomotopyWith f0 f1 P and HomotopyWith f1 f0 P.

Русский

Отображение Symm взаимно однозначно между HomotopyWith f0 f1 P и HomotopyWith f1 f0 P.

LaTeX

$$There is a bijection: HomotopyWith f0 f1 P ≃ HomotopyWith f1 f0 P given by Symm.$$

Lean4

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

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