IntervalCharts

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

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

A space charted on the half-line with interval targets.

• 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

theorem OneMfld.ioi_unbounded (x : NNReal) : ¬Bornology.IsBounded (Set.Ioi x)

theorem OneMfld.univ_unbounded : ¬Bornology.IsBounded Set.univ

@[instance_reducible]

noncomputable def OneMfld.intervalCharted {M : Type u_1} [TopologicalSpace M] (ht : NicelyChartedSpace NNReal M) : IntervalChartedSpace M

Regard an atlas with bounded connected targets as an interval atlas.

Equations

• OneMfld.intervalCharted ht = { toChartedSpace := ht.toChartedSpace, is_interval := ⋯ }