English
The heterogeneous differential hfdifferential is a general construction giving a linear map between PointDerivation and ContMDiffMap derivatives under a matched evaluation hypothesis h: f x = y.
Русский
Гетерогенный дифференциал hfdifferential строит линейное отображение между точечными деривациями и деривациями гладких отображений при условии согласованности значений.
LaTeX
$$$$ hfdifferential: \{f: ContMDiffMap I I' M M'\} \to \ smallsetminus \text{conditions} $$$$
Lean4
/-- The homogeneous differential as a linear map, denoted as `𝒅` within the `Manifold` namespace. -/
def fdifferential (f : C^∞⟮I, M; I', M'⟯) (x : M) : PointDerivation I x →ₗ[𝕜] PointDerivation I' (f x) :=
hfdifferential
(rfl : f x = f x)
-- Standard notation for the differential. The abbreviation is `MId`.
