uniqueMDiffWithinAt_iff_inter_range

English

For any s ⊆ M and x ∈ M, the property UniqueMDiffWithinAt I s x is equivalent to a standard differentiability condition on the preimage of s under extChartAt together with range I.

Русский

Для любой пары s ⊆ M и точки x свойство UniqueMDiffWithinAt I s x эквивалентно дифференцируемости в предобразе s под extChartAt и пересечении с областью диапазона I.

LaTeX

$$$UniqueMDiffWithinAt I s x \;\Leftrightarrow\; UniqueDiffWithinAt 𝕜\, ((extChartAt I x).symm^{-1} s \cap \text{ range } I) ((extChartAt I x) x)$$$

Lean4

theorem uniqueMDiffWithinAt_iff_inter_range {s : Set M} {x : M} :
    UniqueMDiffWithinAt I s x ↔ UniqueDiffWithinAt 𝕜 ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x) :=
  Iff.rfl

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