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.
An arbitrary disjoint union of second-countable manifolds need not be second-countable
Statement
False claim: an arbitrary disjoint union of second-countable manifolds is second-countable.
Facts & Assumptions
Given: An uncountable set and the disjoint union of one-point manifolds.
In the disjoint union topology, a subset of is open exactly when each trace on each summand is open (The disjoint union (coproduct) with the final topology of the canonical injections: a set is open exactly when each of its traces is).
A space is second countable when it has an at most countable basis (Second countability: an at most countable basis for the topology).
The countable-union theorem on the A page requires the index set to be at most countable (Countable disjoint unions of fixed-dimensional smooth manifolds are smooth manifolds).
Refutation
Each singleton is open in : its trace on the [F1] -th summand is the whole one-point space, and on every other summand it is empty, so [F1] makes it open. Thus is an uncountable discrete space.
If were a basis of , then for each the open set [step 1.1, assume-hyp] would contain some with , forcing . Distinct points therefore require distinct basis elements, so every basis is uncountable.
Hence is not second countable by [F2]. This is exactly why [L1] keeps the countability hypothesis explicit.
Depends on
Used by
Dependency tree · two levels
16 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
- Rob van der Vorst, Introduction to differentiable manifolds, §1 (standard reference, not scraped)
- Nigel Hitchin, Differentiable Manifolds, §2.3 (standard reference, not scraped)