UniqueMDiffOn — Mathlib

English

Predicate: at a point x and a set s, there is at most one differentiable derivative within the chart coordinates.

Русский

Свойство: в точке x и для множества s существует по существу единственная производная в координатах карты.

LaTeX

$$$\\text{UniqueMDiffWithinAt } I\: s\\: x := \\text{UniqueDiffWithinAt } \\mathbb{K} ((\\text{extChartAt } I x)^{-1} s \\cap \\text{range } I) ((\\text{extChartAt } I x) x).$$$

Lean4

/-- Predicate ensuring that, at all points of a set, a function can have at most one derivative. -/
def UniqueMDiffOn (s : Set M) :=
  ∀ x ∈ s, UniqueMDiffWithinAt I s x

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