atlas — Mathlib

English

The atlas of charts in a charted space is the collection of all chart maps from the atlas of charts in the space.

Русский

Атлас диаграмм в пространстве ChartedSpace образует совокупность всех отображений диаграмм из атласа.

LaTeX

$$$atlas(H,M) = ChartedSpace.atlas(H,M)$$$

Lean4

/-- The atlas of charts in a `ChartedSpace`. -/
abbrev atlas (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M] [ChartedSpace H M] :
    Set (OpenPartialHomeomorph M H) :=
  ChartedSpace.atlas

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