NeighborhoodCertificate.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.Geometry.exists_uniform_positive_radius line 15
Source documentation
A finite family of positive radii admits a common positive lower bound, including when the indexing type is empty.
```
theorem exists_uniform_positive_radius {ι : Type uIndex} [Finite ι]
    (r : ι → ℝ) (hr : ∀ i, 0 < r i) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ i, δ ≤ r i := by
…
```

theorem OAI.Problem356.Geometry.finite_common_ball line 35

Source documentation

A common ball around a point contained in finitely many open sets. This applies to the open images of the local inverse branches.

theorem finite_common_ball {ι : Type uIndex} {X : Type uX} [Finite ι] [PseudoMetricSpace X]
    (a : X) (U : ι → Set X) (hU : ∀ i, IsOpen (U i))
    (ha : ∀ i, a ∈ U i) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ i, ball a δ ⊆ U i := by
…

theorem OAI.Problem356.Geometry.finite_disjoint_closedBalls line 46

Source documentation

Distinct finitely many centers admit a common positive radius with pairwise disjoint closed balls.

theorem finite_disjoint_closedBalls {ι : Type uIndex} {X : Type uX} [Finite ι] [MetricSpace X]
    (a : ι → X) (ha : Function.Injective a) :
    ∃ δ : ℝ, 0 < δ ∧ Pairwise (fun i j =>
      Disjoint (closedBall (a i) δ) (closedBall (a j) δ)) := by
…

theorem OAI.Problem356.Geometry.finite_disjoint_closedBalls_subset line 65

Source documentation

One radius may simultaneously separate all components and keep each closed component ball inside a prescribed open neighborhood.

theorem finite_disjoint_closedBalls_subset {ι : Type uIndex} {X : Type uX} [Finite ι]
    [MetricSpace X] (a : ι → X) (ha : Function.Injective a)
    (U : ι → Set X) (hU : ∀ i, IsOpen (U i))
    (haU : ∀ i, a i ∈ U i) :
    ∃ δ : ℝ, 0 < δ ∧
      (∀ i, closedBall (a i) δ ⊆ U i) ∧
      Pairwise (fun i j => Disjoint (closedBall (a i) δ) (closedBall (a j) δ)) := by
…