LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A compact set inside an open set has a uniform neighborhood radius

Statement

Let $K$ be compact in Euclidean $R^{n}$ and let $V \subseteq R^{n}$ be open with $K \subseteq V$ . There is $δ > 0$ such that for every $x \in K$ , if $∥ y - x ∥_{2} < δ$ , then $y \in V$ . If $K = \emptyset$ , any positive $δ$ works.

Facts & Assumptions

Given: Compactness and openness in the Euclidean metric (Open cover, subcover, compact metric space, and compact subset of a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it); compactness is intrinsic to the subspace metric (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).

[F1]

For each $x \in V$ , openness gives $r > 0$ with $B (x, 2 r) \subseteq V$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

[F2]

Every open cover of compact $K$ has a finite subcover (Open cover, subcover, compact metric space, and compact subset of a metric space, A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).

[F3]

A nonempty finite set of real numbers has a minimum that belongs to the set (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Proof

1.1givenF1F2constructalgebra

If $K = \emptyset$ , take $δ = 1$ . Otherwise form the family of all balls $B (x, r)$ with $x \in K$ , $r > 0$ , and $B (x, 2 r) \subseteq V$ . Each such ball is open: if $z \in B (x, r)$ , then $s = r - ∥ z - x ∥_{2} > 0$ and $B (z, s) \subseteq B (x, r)$ by the triangle inequality. By [F1] this family covers $K$ ; [F2] supplies a finite subcover $B (x_{i}, r_{i})$ , $1 \leq i \leq q$ .

2.1step 1.1F3givenalgebra∎

Since $K \neq \emptyset$ , the finite subcover has at least one ball. The minimum $δ = \min_{1 \leq i \leq q} r_{i}$ belongs to the nonempty finite set of positive radii, so $δ > 0$ by [F3]. Given $x \in K$ and $∥ y - x ∥_{2} < δ$ , choose a covering ball containing $x$ . Then for its index $i$ , $∥ y - x_{i} ∥_{2} \leq ∥ y - x ∥_{2} + ∥ x - x_{i} ∥_{2} < δ + r_{i} \leq 2 r_{i}$ , so $y \in B (x_{i}, 2 r_{i}) \subseteq V$ .

Depends on

Used by

Dependency tree · two levels

41 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. R. Conn, K. Scheinberg, and L. N. Vicente, Introduction to Derivative-Free Optimization, §§2.1–2.2 and ch. 8 (standard reference, not scraped)
Tamara G. Kolda, Robert Michael Lewis, and Virginia Torczon, Optimization by Direct Search, §§3.1–3.6 and Nelder–Mead discussion (standard reference, not scraped)