symm_comp_toContinuousMap — Mathlib

English

For a homeomorphism f, composing its symmetric inverse with f yields the identity on α.

Русский

Для гомеоморфизма f композиция f.symm с f даёт тождество на α.

LaTeX

$$$(f.symm : C(\\beta, \\alpha)).\\text{comp}(f : C(\\alpha, \\beta)) = \\mathrm{ContinuousMap.id}\\,\\alpha$$$

Lean4

/-- Left inverse to a continuous map from a homeomorphism, mirroring `Equiv.symm_comp_self`. -/
@[simp]
theorem symm_comp_toContinuousMap : (f.symm : C(β, α)).comp (f : C(α, β)) = ContinuousMap.id α := by
  rw [← coe_trans, self_trans_symm, coe_refl]

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