Interval charts on a 1-manifold charted on ℝ≥0, and the Overlap relation.

An OChart has an open-interval target Ioo x y (an interior chart); an HChart has a half-open target Iio x (a boundary chart); an IChart is either.

structure OneMfld.OChart (M : Type u_1) [TopologicalSpace M] extends OpenPartialHomeomorph M NNReal : Type u_1

A one-dimensional chart with an open bounded interval as target.

• toFun : M → NNReal
• invFun : NNReal → M
• source : Set M
• target : Set NNReal
• map_source' ⦃x : M⦄ : x ∈ self.source → ↑self.toPartialEquiv x ∈ self.target
• map_target' ⦃x : NNReal⦄ : x ∈ self.target → self.invFun x ∈ self.source
• left_inv' ⦃x : M⦄ : x ∈ self.source → self.invFun (↑self.toPartialEquiv x) = x
• right_inv' ⦃x : NNReal⦄ : x ∈ self.target → ↑self.toPartialEquiv (self.invFun x) = x
• continuousOn_toFun : ContinuousOn (↑self.toPartialEquiv) self.source
• continuousOn_invFun : ContinuousOn self.invFun self.target
• open_source : IsOpen self.source
• open_target : IsOpen self.target
• target_ioo : ∃ (x : NNReal) (y : NNReal), Set.Ioo x y = self.target

structure OneMfld.HChart (M : Type u_1) [TopologicalSpace M] extends OpenPartialHomeomorph M NNReal : Type u_1

A boundary chart with a half-open interval as target.

• toFun : M → NNReal
• invFun : NNReal → M
• source : Set M
• target : Set NNReal
• map_source' ⦃x : M⦄ : x ∈ self.source → ↑self.toPartialEquiv x ∈ self.target
• map_target' ⦃x : NNReal⦄ : x ∈ self.target → self.invFun x ∈ self.source
• left_inv' ⦃x : M⦄ : x ∈ self.source → self.invFun (↑self.toPartialEquiv x) = x
• right_inv' ⦃x : NNReal⦄ : x ∈ self.target → ↑self.toPartialEquiv (self.invFun x) = x
• continuousOn_toFun : ContinuousOn (↑self.toPartialEquiv) self.source
• continuousOn_invFun : ContinuousOn self.invFun self.target
• open_source : IsOpen self.source
• open_target : IsOpen self.target
• target_iio : ∃ (x : NNReal), Set.Iio x = self.target

structure OneMfld.IChart (M : Type u_1) [TopologicalSpace M] extends OpenPartialHomeomorph M NNReal : Type u_1

A chart whose target is an open interval or a half-open interval.

• toFun : M → NNReal
• invFun : NNReal → M
• source : Set M
• target : Set NNReal
• map_source' ⦃x : M⦄ : x ∈ self.source → ↑self.toPartialEquiv x ∈ self.target
• map_target' ⦃x : NNReal⦄ : x ∈ self.target → self.invFun x ∈ self.source
• left_inv' ⦃x : M⦄ : x ∈ self.source → self.invFun (↑self.toPartialEquiv x) = x
• right_inv' ⦃x : NNReal⦄ : x ∈ self.target → ↑self.toPartialEquiv (self.invFun x) = x
• continuousOn_toFun : ContinuousOn (↑self.toPartialEquiv) self.source
• continuousOn_invFun : ContinuousOn self.invFun self.target
• open_source : IsOpen self.source
• open_target : IsOpen self.target
• is_interval : (∃ (x : NNReal) (y : NNReal), Set.Ioo x y = self.target) ∨ ∃ (x : NNReal), Set.Iio x = self.target

def OneMfld.OChart.toIChart {M : Type u_1} [TopologicalSpace M] (a : OChart M) : IChart M

Regard an interior chart as an interval chart.

Equations

• a.toIChart = { toOpenPartialHomeomorph := a.toOpenPartialHomeomorph, is_interval := ⋯ }

def OneMfld.HChart.toIChart {M : Type u_1} [TopologicalSpace M] (a : HChart M) : IChart M

Regard a boundary chart as an interval chart.

Equations

• a.toIChart = { toOpenPartialHomeomorph := a.toOpenPartialHomeomorph, is_interval := ⋯ }

def OneMfld.Overlap {α : Type u_2} (U V : Set α) : Prop

Two sets meet and each has a point outside the other.

Equations

• OneMfld.Overlap U V = ((U ∩ V).Nonempty ∧ (U \ V).Nonempty ∧ (V \ U).Nonempty)

theorem OneMfld.does_overlap' {α : Type u_2} (U V : Set α) (hu : ¬U ⊆ V) : (U \ V).Nonempty

theorem OneMfld.does_overlap {α : Type u_2} (U V : Set α) (h : (U ∩ V).Nonempty) (hu : ¬U ⊆ V) (hv : ¬V ⊆ U) : Overlap U V

theorem OneMfld.overlap_symm {α : Type u_2} {U V : Set α} (h : Overlap U V) : Overlap V U

theorem OneMfld.Overlap.nonempty {α : Type u_2} {U V : Set α} (h : Overlap U V) : Nonempty ↑U ∧ Nonempty ↑V

theorem OneMfld.chart_target_nonempty {M : Type u_1} [TopologicalSpace M] (φ : OpenPartialHomeomorph M NNReal) (h : φ.source.Nonempty) : φ.target.Nonempty

theorem OneMfld.OChart.connected_source {M : Type u_1} [TopologicalSpace M] (a : OChart M) (h : a.source.Nonempty) : IsConnected a.source

theorem OneMfld.HChart.connected_source {M : Type u_1} [TopologicalSpace M] (a : HChart M) (h : a.source.Nonempty) : IsConnected a.source

theorem OneMfld.IChart.connected_source {M : Type u_1} [TopologicalSpace M] (a : IChart M) (h : a.source.Nonempty) : IsConnected a.source