6.41. MappingDegree.LocalSheetDataFromContMDiff🔗

Jacobians.MappingDegree.LocalSheetDataFromContMDiff — source

ofContMDiffMfderivNeZero

LocalSheetData from ContMDiffAt … ω + non-degenerate chart-pullback derivative.

noncomputable def ofContMDiffMfderivNeZero
    {f : X → Y} {x₀ : X} {y₀ : Y}
    (hf : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω f x₀)
    (hxy : f x₀ = y₀)
    (h_deriv :
      deriv ((chartAt ℂ y₀) ∘ f ∘ (chartAt ℂ x₀).symm)
          ((chartAt ℂ x₀) x₀) ≠ 0) :
    LocalSheetData f y₀ x₀