English
A relation between writtenInExtChartAt along a composition holds, showing how chart expressions compose along a chart at x.
Русский
Связь записей в extChartAt по композиции демонстрирует, как координатные выражения компонуются вдоль карты x.
LaTeX
$$$writtenInExtChartAt I I'' x (g \circ f) y = (writtenInExtChartAt I' I'' (f x) g \circ writtenInExtChartAt I I' x f) y$ for appropriate x, f, g, y$$
Lean4
theorem writtenInExtChartAt_comp (h : ContinuousWithinAt f s x) :
{y |
writtenInExtChartAt I I'' x (g ∘ f) y = (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) y} ∈
𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
by
apply
@Filter.mem_of_superset _ _ (f ∘ (extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) _
(extChartAt_preimage_mem_nhdsWithin (h.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _)))
mfld_set_tac
