6.13. MappingDegree.ChartRestrictionToBall🔗

Jacobians.MappingDegree.ChartRestrictionToBall — source

chart_restrict_to_ball

Chart restriction to a metric ball target. For a charted space Y modelled on ℂ and a point x : Y, there exists a radius r > 0 and an OpenPartialHomeomorph Y ℂ whose target is the open ball Metric.ball ((chartAt ℂ x) x) r, whose function coercion equals chartAt ℂ x, and whose source is contained in the original chart source.

theorem chart_restrict_to_ball
    {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    (x : Y) :
    ∃ (r : ℝ) (_ : 0 < r) (φ' : OpenPartialHomeomorph Y ℂ),
      x ∈ φ'.source ∧
      φ'.target = Metric.ball ((chartAt ℂ x) x) r ∧
      (φ' : Y → ℂ) = (chartAt ℂ x : Y → ℂ) ∧
      φ'.source ⊆ (chartAt ℂ x).source