5.3. Surface.ChartedSpaceOfLocalHomeomorph🔗

Jacobians.Surface.ChartedSpaceOfLocalHomeomorph — source

chartAtPreimage

A partial homeomorphism agreeing with f near x, chosen by Classical.choose.

noncomputable def chartAtPreimage {f : X → Y} (hf : IsLocalHomeomorph f)
    (x : X) : OpenPartialHomeomorph X Y

mem_source_chartAtPreimage

lemma mem_source_chartAtPreimage {f : X → Y} (hf : IsLocalHomeomorph f)
    (x : X) : x ∈ (chartAtPreimage hf x).source

eq_chartAtPreimage

lemma eq_chartAtPreimage {f : X → Y} (hf : IsLocalHomeomorph f) (x : X) :
    f = chartAtPreimage hf x

chartedSpacePreimage

Charted space structure on Y induced by a surjective local homeomorphism f : X → Y. The chart at y is the inverse of a partial homeomorphism around a chosen preimage of y. (Distinct from Mathlib's IsLocalHomeomorph.chartedSpace, whose charts are built differently; downstream proofs here depend on the chartAtPreimage _ _ |>.symm normal form.)

noncomputable def chartedSpacePreimage {f : X → Y} (hf : IsLocalHomeomorph f)
    (hs : Function.Surjective f) : ChartedSpace X Y where