toHomeomorphOfContinuousClosed_apply

English

The underlying function of e.toHomeomorphOfContinuousClosed h1 h2 equals e.

Русский

Функция, полученная из непрерывной и замкнутой биекции, совпадает с исходной функцией.

LaTeX

$$$ \\mathrm{toHomeomorphOfContinuousClosed}(e,h_1,h_2) = e $$$

Lean4

@[simp]
theorem toHomeomorphOfContinuousClosed_apply (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) :
    ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂) = e :=
  rfl

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