ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)

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.

The sets $U_{0}, U_{1}, U_{1 / 2}, U_{1 / 4}, U_{3 / 4}$ of the Urysohn construction computed for two disjoint closed subsets of $R$

Example

Take $A : = (- \infty, 0]$ and $B : = [1, \infty)$ in $R$ , disjoint closed sets of the normal space $R$ (In a metric space any two separated sets have disjoint open neighbourhoods, so every metrizable space is completely normal, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). For $r$ a dyadic rational of $[0, 1]$ with $r < 1$ (The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$ ) put

$U_{r} : = (- \infty, \frac{1 + r}{2}), U_{1} : = R .$

These are open, and satisfy $\overline{U_{r}} \subseteq U_{s}$ for every $r < s$ in $D$ and $U_{1} = R$ , so $(U_{r})_{r \in D}$ is a legitimate instance of the family hypothesised in If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used and could arise from the construction inside Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0, 1]$ , and conversely such a space is normal applied to $A, B$ . In particular:

$U_{0} = (- \infty, \frac{1}{2}), U_{1 / 4} = (- \infty, \frac{5}{8}), U_{1 / 2} = (- \infty, \frac{3}{4}), U_{3 / 4} = (- \infty, \frac{7}{8}), U_{1} = R .$

Facts & Assumptions

Given: $A = (- \infty, 0]$ , $B = [1, \infty)$ in $R$ , and $U_{r} : = (- \infty, (1 + r) / 2)$ for dyadic $r < 1$ , $U_{1} : = R$ .

[L1]

$\overline{(- \infty, c)} = (- \infty, c]$ for real $c$ , and $(- \infty, c) \subseteq (- \infty, c^{'})$ exactly when $c \leq c^{'}$ . The closure identity is two lines from the cited items: $(- \infty, c]$ is closed, since its complement $(c, \infty)$ contains an interval $(x - r, x + r)$ around each of its points $x$ (take $r = x - c$ ), which is the open-set criterion of 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 claim 3; and $c$ lies in the closure of $(- \infty, c)$ , since every interval $(c - r, c + r)$ with $r > 0$ meets it, so by A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set claims 1 and 2 the closure of $(- \infty, c)$ is $(- \infty, c]$ exactly. The inclusion clause is immediate from Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length and the order. (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, A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length)

[L2]

$A \subseteq U_{0}$ : every $x \leq 0$ satisfies $x < 1 / 2$ .

Verification

technique · direct

1.1

For dyadic $r < s < 1$ : $\overline{U_{r}} = (- \infty, (1 + r) / 2]$ by [L1], and $(1 + r) / 2 < (1 + s) / 2$ since $r < s$ , so $\overline{U_{r}} \subseteq (- \infty, (1 + s) / 2) = U_{s}$ .

givenL1algebra

1.2

For dyadic $r < 1$ : $\overline{U_{r}} = (- \infty, (1 + r) / 2]$ , and $(1 + r) / 2 < 1$ since $r < 1$ , so $\overline{U_{r}} \subseteq (- \infty, 1) \subseteq R = U_{1}$ .

givenL1algebra

1.3

$A \subseteq U_{0}$ by [L2]; and $B \subseteq R ∖ U_{r}$ for every dyadic $r < 1$ , since $(1 + r) / 2 < 1 \leq x$ for $x \in B$ , so $x \notin U_{r}$ .

givenL2algebra

2.1

By step 1.1 and step 1.2, $\overline{U_{r}} \subseteq U_{s}$ for every $r < s$ in $D$ , and $U_{1} = R$ ; so $(U_{r})_{r \in D}$ satisfies the hypotheses of If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used, and $f (x) : = \inf ({r \in D : x \in U_{r}} \cup {1})$ is continuous $R \to [0, 1]$ . By step 1.3, $A \subseteq f^{- 1} ({0})$ (every $r \geq 0$ works for $x \in A$ , so $f (x) \leq 0$ , and $f \geq 0$ always) and $B \subseteq f^{- 1} ({1})$ (no dyadic $r < 1$ works for $x \in B$ ).

step 1.1step 1.2step 1.3∎

Remarks

The five requested sets are read off the general formula. $U_{0}, U_{1 / 4}, U_{1 / 2}, U_{3 / 4}$ are nested, each strictly inside the next by step 1.1, and $U_{1} = R$ is the point at which the family widens all at once, in line with the discussion in Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0, 1]$ , and conversely such a space is normal's own Remarks of why the recursion tracks $X ∖ B$ rather than $X$ until the very last step.
This is one legitimate family among many. Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0, 1]$ , and conversely such a space is normal never claims uniqueness, and the family here is not literally the output of the dependent-choice recursion in that item's proof — it is a hand-picked family satisfying the same two hypotheses, chosen because its members have closed forms.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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

Urysohn's lemma (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §33 (standard reference, not scraped)

The sets U0,U1,U1/2,U1/4,U3/4U0​,U1​,U1/2​,U1/4​,U3/4​ of the Urysohn construction computed for two disjoint closed subsets of RR