uniqueDiffOn_extChartAt_target — Mathlib

English

The target of extChartAt I x is a set on which a unique differentiable structure exists (over 𝕜).

Русский

Целевая область extChartAt I x является множеством с уникальной дифференцируемостью над 𝕜.

LaTeX

$$$ UniqueDiffOn\\ 𝕜\\ ((\\mathrm{extChartAt}\\ I\\ x).\\mathrm{target})$$$

Lean4

theorem uniqueDiffOn_extChartAt_target (x : M) : UniqueDiffOn 𝕜 (extChartAt I x).target :=
  by
  rw [extChartAt_target]
  exact I.uniqueDiffOn_preimage (chartAt H x).open_target

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