Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)
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.

Mapping path space replacement of a map

Definition

For a continuous map f:XY, let YI=C0(I,Y) with the ordinary compact-open topology. Define Ef={(x,γ)X×YI:γ(0)=f(x)},pf(x,γ)=γ(1),jf(x)=(x,cf(x)), where cy is the constant path with value y. These use the product and subspace topologies of A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice and Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace. They are called the mapping-path space, its endpoint projection, and its constant-path inclusion.

Evaluation is continuous by Interval exponential law and quotient homotopies, so pf is continuous. The constant-path map xcf(x) is continuous by transposing (x,t)f(x); pairing with x and restricting to Ef shows that jf is continuous. Also let rf(x,γ)=x; this is continuous as a restricted product projection. No arbitrary selection of paths is part of these definitions.

For CGWH spaces use the kified path space, k-product and kified indicated subspace instead; the same interval exponential law supplies these maps. Empty X gives empty Ef. If Y is empty then the existence of f already forces X empty. For a one-point domain this is the space of paths starting at its specified image; for a one-point target it identifies with X. The factorization and homotopy claims are proved next.

Depends on

Used by

Dependency tree · two levels

21 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