tangentCoordChange_def — Mathlib

English

If z lies in the intersection of the chart sources, then the derivative of the coordinate change is described by HasFDerivWithinAt for the appropriate map.

Русский

Если z принадлежит пересечению областей источников диаграмм, то производная перехода координат описывается через HasFDerivWithinAt для соответствующей отображения.

LaTeX

$$$$ HasFDerivWithinAt\big((\mathrm{extChartAt} I y) \circ (\mathrm{extChartAt} I x).symm\big)\big( \mathrm{tangentCoordChange} I x y z \big)\big( \mathrm{range} I \big)\big(\mathrm{extChartAt} I x z\big). $$$$

Lean4

theorem tangentCoordChange_def {x y z : M} :
    tangentCoordChange I x y z = fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) :=
  rfl

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