FinitelyCharted

Supporting results for the classification of compact one-dimensional manifolds.

noncomputable def OneMfld.chooseCharts {H : Type u_1} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [CompactSpace M] [ht : ChartedSpace H M] : ↑{ht' : ChartedSpace H M | ChartedSpace.atlas.Finite ∧ ChartedSpace.atlas ⊆ ChartedSpace.atlas}

Choose a finite subatlas covering a compact charted space.

Equations

• One or more equations did not get rendered due to their size.