continuousAt_extChartAt' — Mathlib

English

For any x' in the source, extChartAt I x is continuous at x'.

Русский

Для любого x' из источника extChartAt I x отображение непрерывно в точке x'.

LaTeX

$$$ \\forall x'\\, (x' \\in (\\mathrm{extChartAt} I x).\\mathrm{source}) \\Rightarrow \\\\ \\operatorname{ContinuousAt} (\\mathrm{extChartAt} I x) x'$$$

Lean4

theorem continuousAt_extChartAt' {x x' : M} (h : x' ∈ (extChartAt I x).source) : ContinuousAt (extChartAt I x) x' :=
  continuousAt_extend _ <| by rwa [← extChartAt_source I]

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