toHomeomorphOfIsInducing_symm_apply

English

The inverse of the induced homeomorphism equals the induced homeomorphism of the inverse bijection.

Русский

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

LaTeX

$$$ \\bigl( f.toHomeomorphOfIsInducing hf \\bigr).\\mathrm{symm} = f^{\\mathrm{symm}}.toHomeomorph (\\lambda s. \\dots) $$$

Lean4

@[simp]
theorem toHomeomorphOfIsInducing_symm_apply (f : X ≃ Y) (hf : IsInducing f) :
    ⇑(f.toHomeomorphOfIsInducing hf).symm = f.symm :=
  rfl

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