toContinuousMap_comp_symm — Mathlib

English

For a given homeomorphism f, the map (toContinuousMap f).comp (toContinuousMap f.symm) is the identity on β.

Русский

Для гомеоморфизма f отображение (toContinuousMap f) ∘ (toContinuousMap f.symm) равно тождественному отображению на β.

LaTeX

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

Lean4

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

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