DifferentiableWithinAtProp — Mathlib

English

A property defining differentiability within at a set, read in model coordinates.

Русский

Свойство, задающее дифференцируемость внутри множества в координатах модели.

LaTeX

$$$\text{DifferentiableWithinAtProp } (f) (s) (x) := \text{DifferentiableWithinAt } 𝕜 (I' \circ f \circ I^{-1}) (I x).$$$

Lean4

/-- Property in the model space of a model with corners of being differentiable within at set at a
point, when read in the model vector space. This property will be lifted to manifolds to define
differentiable functions between manifolds. -/
def DifferentiableWithinAtProp (f : H → H') (s : Set H) (x : H) : Prop :=
  DifferentiableWithinAt 𝕜 (I' ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ Set.range I) (I x)

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