ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 of target values gives a compact family of constant maps

Example

Let $X$ be a nonempty locally compact Hausdorff space, let $Y$ be a metric space, and let $Q \subseteq Y$ be compact. For $q \in Q$ , let $c_{q} : X \to Y$ be the constant map with value $q$ . Then $C_{Q} : = {c_{q} : q \in Q}$ is compact in the compact-open topology, and $q \mapsto c_{q}$ is a homeomorphism from $Q$ onto $C_{Q}$ .

Facts & Assumptions

Given: A nonempty locally compact Hausdorff space $X$ , a metric space $Y$ , and a compact subset $Q \subseteq Y$ .

[L1]

Compact-open subbasic sets have the form $S (K, V) = {f : f [K] \subseteq V}$ (The compact-open topology on $C (X, Y)$ for arbitrary topological spaces).

[L2]

A continuous image of a compact space is compact, and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

Verification

technique · direct

1.1L1

Define $Φ : Q \to C (X, Y)$ by $Φ (q) = c_{q}$ . For a subbasic $S (K, V)$ , its inverse image under $Φ$ is $Q$ when $K = \emptyset$ , and is $Q \cap V$ when $K \neq \emptyset$ . Hence $Φ$ is continuous.

1.2L1

Fix $x_{0} \in X$ . Evaluation at $x_{0}$ is continuous because the inverse image of open $V \subseteq Y$ is $S ({x_{0}}, V)$ . Its restriction to $C_{Q}$ is inverse to $Φ$ .

2.1L2step 1.1

By [L2], the image $C_{Q} = Φ [Q]$ is compact.

3.1step 1.1step 2.1step 1.2∎

Therefore $Φ : Q \to C_{Q}$ is a homeomorphism, and step 2.1 gives the asserted compactness.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Topology, second edition, Section 47 (standard reference, not scraped)