ChartChain: a Lebesgue-number chart subdivision along a path (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §3.1). A subdivision of [0,1] with chart-and-ball data adapted to a path γ, obtained from mathlib's 1D Lebesgue-number lemma exists_monotone_Icc_subset_open_cover_unitInterval applied to the cover of I by preimages of chart-balls along γ.

Main declarations:

• RS.ChartChain γ — the subdivision structure.
• RS.exists_chartChain — existence, for any continuous path γ.

structure RS.ChartChain {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x y : X} (γ : Path x y) : Type u_1

A subdivision of [0,1] with chart-and-ball data adapted to γ: on each piece Icc (t k) (t (k+1)), γ stays inside a single chart e k with image inside a ball ball (c k) (r k) ⊆ (e k).target.

• n : ℕ

  The number of steps in the chain.

• t : ℕ → ℝ

  The subdivision times.

• ht0 : self.t 0 = 0
• ht1 (k : ℕ) : self.n ≤ k → self.t k = 1
• mono : Monotone self.t
• e : ℕ → OpenPartialHomeomorph X ℂ

  The chart used on each step.

• he (k : ℕ) : self.e k ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X
• c : ℕ → ℂ

  The centre of each step's disc, in that step's chart.

• r : ℕ → ℝ

  The radius of each step's disc.

• hr (k : ℕ) : 0 < self.r k
• ball_subset (k : ℕ) : Metric.ball (self.c k) (self.r k) ⊆ (self.e k).target
• maps (k : ℕ) (u : ℝ) : u ∈ Set.Icc (self.t k) (self.t (k + 1)) → γ.extend u ∈ (self.e k).source ∧ ↑(self.e k) (γ.extend u) ∈ Metric.ball (self.c k) (self.r k)

theorem RS.exists_chartChain {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) : Nonempty (ChartChain γ)