coe_refl — Mathlib

English

The identity homeomorphism on α corresponds to the identity continuous map on α.

Русский

Идентичность гомеоморфизма на α соответствует идентичному непрерывному отображению на α.

LaTeX

$$$(\\mathrm{Homeomorph.refl}\\,\\alpha : C(\\alpha,\\alpha)) = \\mathrm{ContinuousMap.id}\\,\\alpha$$$

Lean4

@[simp]
theorem coe_refl : (Homeomorph.refl α : C(α, α)) = ContinuousMap.id α :=
  rfl

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