UnitSeparatedNet.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PolycyclicRecognition.exists_unit_separated_net line 20
Source documentation
A maximal unit-separated set covers the whole metric space by closed unit balls. No measure or geometric input is required for this step.
```
theorem exists_unit_separated_net :
    ∃ V : Set X, V.Pairwise (fun x y => 1 < dist x y) ∧
      ∀ x : X, ∃ v ∈ V, dist x v ≤ 1 := by
…
```
theorem OAI.PolycyclicRecognition.finite_separated_subset_of_compact line 41
Source documentation
Compact sets contain only finitely many points of a unit-separated set.
```
theorem finite_separated_subset_of_compact {V K : Set X}
    (hV : V.Pairwise (fun x y => 1 < dist x y)) (hK : IsCompact K) (hVK : V ⊆ K) :
    V.Finite := by
…
```
theorem OAI.PolycyclicRecognition.finite_unit_net_ball line 69
Source documentation
Every bounded part of the net is finite, giving the local finiteness needed to glue the cutoff partitions.
```
theorem finite_unit_net_ball [ProperSpace X] {V : Set X}
    (hV : V.Pairwise (fun x y => 1 < dist x y)) (x : X) (R : ℝ) :
    (V ∩ Metric.closedBall x R).Finite :=
…
```