FiniteIntervalCharts

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

class OneMfld.FinitelyIntervalChartedSpace (M : Type u_1) [TopologicalSpace M] extends OneMfld.IntervalChartedSpace M : Type u_1

A space equipped with a finite atlas of interval charts.

• atlas : Set (OpenPartialHomeomorph M NNReal)
• chartAt : M → OpenPartialHomeomorph M NNReal
• mem_chart_source (x : M) : x ∈ (ChartedSpace.chartAt x).source
• chart_mem_atlas (x : M) : ChartedSpace.chartAt x ∈ ChartedSpace.atlas
• is_interval (φ : OpenPartialHomeomorph M NNReal) (h : φ ∈ ChartedSpace.atlas) : (∃ (x : NNReal) (y : NNReal), Set.Ioo x y = φ.target) ∨ ∃ (x : NNReal), Set.Iio x = φ.target
• is_finite : ChartedSpace.atlas.Finite

@[instance_reducible]

noncomputable def OneMfld.finitelyIntervalCharted {M : Type u_1} [TopologicalSpace M] [CompactSpace M] (ht : IntervalChartedSpace M) : FinitelyIntervalChartedSpace M

Extract a finite interval atlas from compactness.

Equations

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