PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 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.

Under choice, for $Y \subseteq X$ , $w (Y) \leq w (X)$ and $χ (y, Y) \leq χ (y, X)$

Statement

Assuming choice, $Y \subseteq X$ implies $w (Y) \leq w (X)$ and $χ (y, Y) \leq χ (y, X)$ for $y \in Y$ .

Facts & Assumptions

Given: A subspace $Y \subseteq X$ , a basis $B$ of $X$ of cardinality $w (X)$ , and a local base $N_{y}$ at $y \in Y$ of cardinality $χ (y, X)$ .

[L1]

In the subspace topology, the open subsets of $Y$ are the traces $U \cap Y$ of open subsets $U$ of $X$ (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).

[L2]

Weight is the least cardinality of a basis and local character is the least cardinality of a neighbourhood base at a point (Under choice, weight $w (X)$ , density $d (X)$ , local character $χ (x, X)$ , and character $χ (X)$ as raw cardinal minima and a supremum).

Proof

technique · direct

1.1

The family ${B \cap Y : B \in B}$ is a basis of $Y$ by [L1] and has cardinality at most $∣ B ∣ = w (X)$ .

1.2

The family ${N \cap Y : N \in N_{y}}$ is a local base at $y$ in $Y$ by [L1] and has cardinality at most $∣ N_{y} ∣ = χ (y, X)$ .

2.1

Applying the two minima in [L2] to the families of steps 1.1 and 1.2 yields $w (Y) \leq w (X)$ and $χ (y, Y) \leq χ (y, X)$ .

step 1.1step 1.2L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

D. H. Fremlin, Measure Theory, Chapter 5A (standard reference, not scraped)

Under choice, for Y⊆XY⊆X, w(Y)≤w(X)w(Y)≤w(X) and χ(y,Y)≤χ(y,X)χ(y,Y)≤χ(y,X)