Theorems · Inductive type · manifolds

ChartedSpace

(H : Type u_5) → [TopologicalSpace H] → (M : Type u_6) → [TopologicalSpace M] → Type (max u_5 u_6)

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

Cited by

2,397 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace