uniqueMDiffWithinAt_iff — Mathlib

English

For any chart I, the unique MDiff property at s is equivalent to a corresponding unique MDiff property in coordinates via extChartAt.

Русский

Для чарта I уникальная MDiff-свойство в s эквивалентно соответствующему свойству в координатах через extChartAt.

LaTeX

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

Lean4

theorem uniqueMDiffWithinAt_iff {s : Set M} {x : M} :
    UniqueMDiffWithinAt I s x ↔
      UniqueDiffWithinAt 𝕜 ((extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target) ((extChartAt I x) x) :=
  by
  apply uniqueDiffWithinAt_congr
  rw [nhdsWithin_inter, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]

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