English
If M is modeled by H' and H' is modeled by H, then M can be modeled by H with atlas dada built from the atlas of H' M and atlas H H'.
Русский
Если M моделируется через H', а H' - через H, то M может моделироваться через H, используя каноническое построение атласа.
LaTeX
$$ChartedSpace.comp (H) (H') (M) ...$$
Lean4
/-- If `M` is modelled on `H'` and `H'` is itself modelled on `H`, then we can consider `M` as being
modelled on `H`. -/
def comp (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H'] (M : Type*) [TopologicalSpace M]
[ChartedSpace H H'] [ChartedSpace H' M] : ChartedSpace H M
where
atlas := image2 OpenPartialHomeomorph.trans (atlas H' M) (atlas H H')
chartAt p := (chartAt H' p).trans (chartAt H (chartAt H' p p))
mem_chart_source p := by simp only [mfld_simps]
chart_mem_atlas p := ⟨chartAt _ p, chart_mem_atlas _ p, chartAt _ _, chart_mem_atlas _ _, rfl⟩
