PointDerivation — Mathlib

English

The PointDerivation abbreviation identifies the derivations at a point x with Derivation 𝕜 of the function algebra.

Русский

Упрощение PointDerivation представляет деривации в точке x как Derivation 𝕜 от соответствующей алгебры функций.

LaTeX

$$$$ \text{PointDerivation}(x) \;:=\; \mathrm{Derivation}_{\mathbb{K}}(C^∞(I,M;\mathbb{K})⟨x⟩, \mathbb{K}). $$$$

Lean4

/-- The derivations at a point of a manifold. Some regard this as a possible definition of the
tangent space, as this coincides with the usual tangent space for finite-dimensional `C^∞` real
manifolds. The identification is not true in general, though. -/
abbrev PointDerivation (x : M) :=
  Derivation 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜

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