toHomeomorphOfFiniteDimensional — Mathlib

English

Reinterpret an affine equivalence as a homeomorphism.

Русский

Переопределение аффинной эквивалентности как гомеоморфизма.

LaTeX

$$$ f.toHomeomorphOfFiniteDimensional : PE \simeq PF $$$

Lean4

/-- Reinterpret an affine equivalence as a homeomorphism. -/
def toHomeomorphOfFiniteDimensional (f : PE ≃ᵃ[𝕜] PF) : PE ≃ₜ PF
    where
  toEquiv := f.toEquiv
  continuous_toFun := f.continuous_of_finiteDimensional
  continuous_invFun :=
    haveI : FiniteDimensional 𝕜 F := f.linear.finiteDimensional
    f.symm.continuous_of_finiteDimensional

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