Structures · Geometry

ChartedSpace

A charted space is a topological space endowed with an atlas, i.e., a set of local homeomorphisms taking values in a model space H, called charts, such that the domains of the charts cover the whole space. We express the covering property by choosing for each x a member chartAt x of the atlas containing x in its source: in the smooth case, this is convenient to construct the tangent bundle in an efficient way. The model space is written as an explicit parameter as there can be several model spaces for a given topological space. For instance, a complex manifold (modelled over ℂ^n) will also be seen sometimes as a real manifold over ℝ^(2n).

Defined in

Mathlib.Geometry.Manifold.ChartedSpace

Shape

2 explicit arguments · adds atlas, chartAt, mem_chart_source, chart_mem_atlas