MDifferentiableOn — Mathlib

English

A function between manifolds differentiable on a set s if it is differentiable at every point of s.

Русский

Функция между манефолдными пространствами дифференцируема на множестве s, если дифференцируема в каждой точке множества.

LaTeX

$$MDifferentiableOn (f) (s) := ∀ x ∈ s, MDifferentiableWithinAt I I' f s x$$

Lean4

/-- `MDifferentiableOn I I' f s` indicates that the function `f` between manifolds
has a derivative within `s` at all points of `s`.
This is a generalization of `DifferentiableOn` to manifolds. -/
def MDifferentiableOn (f : M → M') (s : Set M) :=
  ∀ x ∈ s, MDifferentiableWithinAt I I' f s x

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