toHomeomorphOfContinuousOpen_symm_apply

English

The inverse of the continuous-open induced homeomorphism equals the inverse bijection's homeomorphism.

Русский

Обратный к полученному непрерывно-открытому гомеоморфизму равен гомеоморфизму обратной биекции.

LaTeX

$$$ \\bigl( e.toHomeomorphOfContinuousOpen h_1 h_2 \\bigr).\\mathrm{symm} = e.symm.toHomeomorph (\\lambda s. \\dots) $$$

Lean4

@[simp]
theorem toHomeomorphOfContinuousOpen_symm_apply (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) :
    ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂).symm = e.symm :=
  rfl

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