MovingPointedLimitProper.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Properness of the sampled limit for moving centers

The uniform finite nets pass to the distance-matrix limit. Density then extends their covers to its metric completion, proving properness.

theorem OAI.RegularPointCoordinates.MovingRescalingNetFamily.sample_limit_cover line 27

Source documentation

A finite net in the sample metric survives passage to the limit.

theorem sample_limit_cover (R k : ℕ) (a : s.Index)
    (ha : dist a none < (R:ℝ)+1) :
    ∃ j : Fin (s.size R k), dist a (some ⟨R,k,j⟩) ≤ 1/((k:ℝ)+1) := by
…

theorem OAI.RegularPointCoordinates.MovingRescalingNetFamily.completion_limit_cover line 49

Source documentation

The completed limit has the same finite covers, with twice the mesh.

theorem completion_limit_cover (R k : ℕ)
    (y : UniformSpace.Completion s.Index)
    (hy : dist y (none : s.Index) ≤ R) :
    ∃ j : Fin (s.size R k),
      dist y ((some ⟨R,k,j⟩ : s.Index) : UniformSpace.Completion s.Index) <
        2/((k:ℝ)+1) := by
…

theorem OAI.RegularPointCoordinates.MovingRescalingNetFamily.completion_proper line 77
Source documentation
Completing the sampled pseudometric gives a proper metric space.
```
theorem completion_proper : ProperSpace (UniformSpace.Completion s.Index) := by
…
```