Theorems · Definition · global analysis

hfdifferential

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                {I' : ModelWithCorners 𝕜 E' H'} →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {f : ContMDiffMap I I' M M' ↑⊤} →
                                          {x : M} → {y : M'} → f x = y → PointDerivation I x →ₗ[𝕜] PointDerivation I' y

The heterogeneous differential as a linear map, denoted as 𝒅ₕ within the Manifold namespace. Instead of taking a function as an argument, this differential takes h : f x = y. It is particularly handy for situations where the points at which it has to be evaluated are equal but not definitionally equal.

Defined in

Mathlib.Geometry.Manifold.DerivationBundle

Cited by

10 results in Mathlib

Foundations

Depth 229 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace