English
For a topological base B and a normed vector space F, a map φ sending each base point to a linear isomorphism of F determines an open partial homeomorphism of B × F to itself, acting fiberwise by φ(b). This defines an open partial homeomorphism whose domain is U × F and whose action on fibers is given by φ(b).
Русский
Для основания B с топологией и нормированного пространства F карта φ, присваивающая каждой точке базиса линейное изоморфизмное отображение F, задает октовую частично взаимнооднозначную отображение B × F в себя, действующее по волокнам как φ(b).
LaTeX
$$$\\text{Given } U\\subset B \\,\\text{open},\\ h: COnst,\\quad (b,v)\\mapsto (b,\\phi(b)[v])$ defines a open partial homeomorphism $B\\times F \\to B\\times F$ with source/target $U\\times\\mathbb{R}^n$ (fiberwise).$$
Lean4
/-- For `B` a topological space and `F` a `𝕜`-normed space, a map from `U : Set B` to `F ≃L[𝕜] F`
determines an open partial homeomorphism from `B × F` to itself by its action fiberwise. -/
def openPartialHomeomorph (φ : B → F ≃L[𝕜] F) (hU : IsOpen U) (hφ : ContinuousOn (fun x => φ x : B → F →L[𝕜] F) U)
(h2φ : ContinuousOn (fun x => (φ x).symm : B → F →L[𝕜] F) U) : OpenPartialHomeomorph (B × F) (B × F)
where
toFun x := (x.1, φ x.1 x.2)
invFun x := (x.1, (φ x.1).symm x.2)
source := U ×ˢ univ
target := U ×ˢ univ
map_source' _x hx := mk_mem_prod hx.1 (mem_univ _)
map_target' _x hx := mk_mem_prod hx.1 (mem_univ _)
left_inv' _ _ := Prod.ext rfl (ContinuousLinearEquiv.symm_apply_apply _ _)
right_inv' _ _ := Prod.ext rfl (ContinuousLinearEquiv.apply_symm_apply _ _)
open_source := hU.prod isOpen_univ
open_target := hU.prod isOpen_univ
continuousOn_toFun :=
have : ContinuousOn (fun p : B × F => ((φ p.1 : F →L[𝕜] F), p.2)) (U ×ˢ univ) := hφ.prodMap continuousOn_id
continuousOn_fst.prodMk (isBoundedBilinearMap_apply.continuous.comp_continuousOn this)
continuousOn_invFun :=
have : ContinuousOn (fun p : B × F => (((φ p.1).symm : F →L[𝕜] F), p.2)) (U ×ˢ univ) := h2φ.prodMap continuousOn_id
continuousOn_fst.prodMk (isBoundedBilinearMap_apply.continuous.comp_continuousOn this)
