LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31

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.

Homotopy relative to a subspace is reflexive and symmetric

Statement

Let $A \subseteq X$ . Every continuous map $f : X \to Y$ is homotopic to itself rel $A$ . If $f ≃_{A} g$ , then $g ≃_{A} f$ .

Facts & Assumptions

Given: Topological spaces $X, Y$ , a subspace $A \subseteq X$ , continuous maps $f, g : X \to Y$ , and, for symmetry, a homotopy $H : X \times I \to Y$ from $f$ to $g$ rel $A$ .

[A1]

A homotopy rel $A$ is a continuous $K : X \times I \to Y$ with $K (x, 0)$ and $K (x, 1)$ the prescribed endpoint maps and $K (a, t)$ equal to their common value for every $a \in A$ and $t \in I$ (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

[L1]

The projections from a product are continuous, and a map into a product is continuous exactly when all of its components are continuous (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).

[L2]

A map is continuous exactly when preimages of open sets are open (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , condition (b)).

[L3]

In the usual topology of $R$ , the open balls are the intervals $(u - r, u + r)$ ; $I = [0, 1]$ has the subspace topology (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, 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).

Proof

technique · direct

1.1

The projection $p_{X} : X \times I \to X$ is continuous by [L1]. For every open $V \subseteq Y$ , $(f \circ p_{X})^{- 1} [V] = p_{X}^{- 1} [f^{- 1} [V]]$ is open, so $K_{f} (x, t) : = f (x)$ is continuous by [L2].

L1L2

1.2

The map $r : I \to I$ , $r (t) = 1 - t$ , is continuous: for $t_{0} \in I$ and an open neighbourhood $V = O \cap I$ of $r (t_{0})$ , with $O$ open in $R$ , [L3] gives $ε > 0$ with $(r (t_{0}) - ε, r (t_{0}) + ε) \subseteq O$ ; then $U = (t_{0} - ε, t_{0} + ε) \cap I$ is an open neighbourhood of $t_{0}$ and $r [U] \subseteq V$ , since $∣ r (t) - r (t_{0}) ∣ = ∣ t - t_{0} ∣$ .

2.1

The homotopy $K_{f}$ has $K_{f} (x, 0) = K_{f} (x, 1) = f (x)$ and $K_{f} (a, t) = f (a)$ for $a \in A$ , so it is a homotopy from $f$ to itself rel $A$ .

step 1.1A1

2.2

The map $R : X \times I \to X \times I$ , $R (x, t) = (x, r (t))$ , is continuous because its components are continuous by step 1.2 and [L1]. For every open $V \subseteq Y$ , $(H \circ R)^{- 1} [V] = R^{- 1} [H^{- 1} [V]]$ is open, so $\overline{H} : = H \circ R$ is continuous by [L2].

step 1.2L1L2

3.1

One has $\overline{H} (x, 0) = H (x, 1) = g (x)$ and $\overline{H} (x, 1) = H (x, 0) = f (x)$ ; for $a \in A$ , $\overline{H} (a, t) = H (a, 1 - t) = f (a) = g (a)$ . Hence $\overline{H}$ is a homotopy from $g$ to $f$ rel $A$ .

step 2.2A1∎

Depends on

Used by

Homotopy relative to a fixed subspace, and path homotopy relative to endpoints, are equivalence relations Corollary

Dependency tree · two levels

32 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. Hatcher, Algebraic Topology, Section 0 (standard reference, not scraped)
Homotopy lecture notes (University of Padua) (standard reference, not scraped)