chartAt_comp — Mathlib

English

The chart at x for the composed space equals the composition of charts: chartAt H x = chartAt H' x trans chartAt H (chartAt H' x x).

Русский

Карта chartAt для композиции равна композиции карт: chartAt H x = chartAt H' x ∘ chartAt H (chartAt H' x x).

LaTeX

$$chartAt H x = (chartAt H' x) .trans (chartAt H (chartAt H' x x))$$

Lean4

theorem chartAt_comp (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H'] {M : Type*}
    [TopologicalSpace M] [ChartedSpace H H'] [ChartedSpace H' M] (x : M) :
    (letI := ChartedSpace.comp H H' M;
      chartAt H x) =
      chartAt H' x ≫ₕ chartAt H (chartAt H' x x) :=
  rfl

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