Proper.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Properness from the actual curvature-dimension volume bound

The existing FullCD.ball_ratio theorem bounds the mass of every small ball centered in a bounded region from below. Disjoint small balls therefore bound every separated set. The resulting finite nets prove total boundedness; completeness then gives properness. No compactness hypothesis is added.

theorem OAI.RegularPointCoordinates.separated_encard_le_of_finset_bound line 23
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.totallyBounded_closedBall line 45
Source documentation
Every bounded ball is totally bounded, directly from CD volume comparison.
```
theorem NoncollapsedRCD.totallyBounded_closedBall {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) (R : ℝ) :
    TotallyBounded (closedBall p R) := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.properSpace line 116
Source documentation
The proper-space assumption of the conditional chart theorem is itself an RCD consequence in the manuscript's dimension range.
```
theorem NoncollapsedRCD.properSpace {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) : ProperSpace X := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD