OAI/Analysis/CircleDomains/Topology/CircleChainRule.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pullback of the intrinsic circle differential

The ordinary real chain rule applies to a local real lift. Independence of that lift identifies the result with the intrinsic circle differential.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv_comp line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.planeDerivativeMatrix_eq_columns line 34
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.real_covector_apply line 42
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_comp_vector line 49