Theorems · Definition · manifolds

chartAt

(H : Type u_5) →
  [inst : TopologicalSpace H] →
    {M : Type u_6} → [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → M → OpenPartialHomeomorph M H

The preferred chart at a point x in a charted space M.

Defined in

Mathlib.Geometry.Manifold.ChartedSpace

Cited by

301 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 5 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceChartedSpace