symm_toHomeomorph — Mathlib

English

The inverse of a continuous linear equivalence as a homeomorph is the inverse of the original homeomorph.

Русский

Обратное непрерывное линейное эквивалентное отображение как гомеоморфизм — это обратное исходного гомеоморфизма.

LaTeX

$$$e.toHomeomorph^{-1} = e^{-1}.toHomeomorph$$$

Lean4

@[deprecated "use instead `toHomeomorph_symm`, in the reverse direction" (since := "2025-06-08")]
theorem symm_toHomeomorph (e : M₁ ≃SL[σ₁₂] M₂) : e.toHomeomorph.symm = e.symm.toHomeomorph :=
  rfl

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