equiv_refl — Mathlib

English

The equivalence induced by the identity homeomorphism is the identity equivalence on Compacts α.

Русский

Эквиваленция, полученная от тождественного гомеоморфизма, является тождественной эквиваленцией на Compacts α.

LaTeX

$$$\\mathrm{Compacts}\\,\\mathrm{equiv}(\\mathrm{Homeomorph.refl }\\alpha) = \\mathrm{Equiv.refl} (\\mathrm{Compacts }\\alpha).$$$

Lean4

@[simp]
theorem equiv_refl : Compacts.equiv (Homeomorph.refl α) = Equiv.refl _ :=
  Equiv.ext map_id

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