LocalCoordinateExtension.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable extensions preserving the local metric approximation

theorem OAI.RegularPointCoordinates.IsPointedApproximation.congr_on_ball line 15

Source documentation

Only values on the closed testing ball enter a pointed approximation.

theorem IsPointedApproximation.congr_on_ball {Y : Type*} [MetricSpace Y]
    {p : X} {q : Y} {r R ε : ℝ} {f g : X → Y}
    (hRr : 0 ≤ R * r) (hf : IsPointedApproximation p q r R ε f)
    (hfg : EqOn f g (closedBall p (R * r))) :
    IsPointedApproximation p q r R ε g := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.exists_measurable_local_extension line 31
Source documentation
A continuous local coordinate map has a measurable extension which agrees pointwise throughout its open domain.
```
theorem exists_measurable_local_extension [MeasurableSpace X] [BorelSpace X]
    {n : ℕ} {s : Set X} (hs : MeasurableSet s) {v : X → Euclidean n}
    (hv : ContinuousOn v s) :
    ∃ v' : X → Euclidean n, Measurable v' ∧ EqOn v v' s := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean