toHomeomorph — Mathlib

English

If I is boundaryless, then H and E are homeomorphic via the map I.toFun' with inverse I.symm.toFun.

Русский

Если I без границы, то пространства H и E гомеоморфны через отображение I.toFun' с обратным I.symm.toFun.

LaTeX

$$$H \cong E$ (homeomorphism given by I)$$

Lean4

/-- If `I` is a `ModelWithCorners.Boundaryless` model, then it is a homeomorphism. -/
@[simps +simpRhs]
def toHomeomorph {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] : H ≃ₜ E
    where
  __ := I
  left_inv := I.left_inv
  right_inv _ := I.right_inv <| I.range_eq_univ.symm ▸ mem_univ _

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