PointedApproximationLifts.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Convergent lifts of interior Euclidean points

The lifts use the density clause of the prescribed approximation maps. They need not be measurable: they are only countable point sequences.

theorem OAI.RegularPointCoordinates.pointed_convergent_lift line 17

theorem OAI.RegularPointCoordinates.pointed_uniform_values_tendsto line 44

Source documentation

Uniform convergence through the given coordinate maps determines values on every convergent lift in the physical working balls.

theorem pointed_uniform_values_tendsto {n : ℕ} {S : ℝ}
    (p : ℕ → X) (r : ℕ → ℝ) (v : ℕ → X → Euclidean n)
    (u : ℕ → X → ℝ) {f : Euclidean n → ℝ} (hf : Continuous f)
    (hu : ∀ δ : ℝ, 0<δ → ∀ᶠ k in atTop, ∀ x,
      dist x (p k)≤S*r k → |u k x-f (v k x)|<δ)
    (x : ℕ → X) (hx : ∀ᶠ k in atTop, dist (x k) (p k)≤S*r k)
    {z : Euclidean n} (hz : Tendsto (fun k => v k (x k)) atTop (𝓝 z)) :
    Tendsto (fun k => u k (x k)) atTop (𝓝 (f z)) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean