Theorems · Theorem · manifolds

mem_chart_target

∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), ↑(chartAt H x) x ∈ (chartAt H x).target

Defined in

Mathlib.Geometry.Manifold.ChartedSpace

Cited by

5 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceChartedSpace