refl_toOpenPartialHomeomorph — Mathlib

English

The restriction of a Homeomorph's identity to an OpenPartialHomeomorph equals the identity-induced OpenPartialHomeomorph.

Русский

Ограничение тождественной гомеоморфии до OpenPartialHomeomorph совпадает с тождественным OpenPartialHomeomorph.

LaTeX

$$$(Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X$$$

Lean4

@[simp, mfld_simps]
theorem refl_toOpenPartialHomeomorph : (Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X :=
  rfl

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