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.
Fleissner's construction of a normal nonmetrizable Moore space from level data
Statement
Let be an infinite cardinal, let be increasing with for every and , let , and let be stationary in . Fix, for each , an increasing sequence of nonlimit ordinals cofinal in (Fleissner's HYP covering interface), and assume the ladder separation conclusion of Fleissner's Lemma 1: for every there is such that for all distinct and all .
Then there is a normal nonmetrizable Moore space (Moore spaces and developments, Metrizable spaces are collectionwise normal). The same space carries the stated uniform base, hence is metacompact.
Facts & Assumptions
Given: and the ladders as in the Statement. By passing to a cofinal tail-subsequence and then prepending , we may and do assume that , that for , and, when , that every with is infinite. These reindexings preserve the power bounds and the supremum .
is a regular cardinal with ; sums and products of infinite cardinals absorb, in particular . From the given and the cardinal exponent laws, for every cardinal with one has (Cardinal (initial ordinal) and cardinality, Cardinal sum , product and exponentiation , and why they are written apart from the ordinal operations, Absorption: for cardinals with infinite and , , and when , Assuming the Axiom of Choice, , and Cantor's theorem in cardinal form: ).
Every set can be well-ordered, so a set of cardinality can be enumerated as (Well-order and well-ordered set, Injection, surjection, bijection, The Axiom of Choice).
Clubs and stationary sets in : a set is closed if it contains the sup of each of its bounded subsets, clubs are the closed unbounded sets, stationary means meeting every club; a club is stationary; supersets of stationary sets are stationary; a stationary set minus a non-stationary set is stationary; and a countable union of non-stationary subsets of is non-stationary (Closed unbounded subsets of ordinals, The club filter and nonstationary ideal, Basic stationary-set calculus).
Fodor's pressing-down lemma: if is stationary and is regressive ( throughout), then some fibre of is stationary (Fodor’s pressing-down lemma, Regressive functions on ordinals).
For the Erdős–Rado theorem gives , and for the infinite Ramsey theorem gives for every finite ; the arrow means that every colouring of pairs admits a homogeneous set of the target size (Erdős–Rado for arbitrary infinite cardinals and finite arity, Infinite Ramsey theorem for fixed finite arity and colors, Partition arrows and homogeneous sets, Cardinal (initial ordinal) and cardinality).
Moore spaces, developments, stars, and first countability; regular spaces; metrizable spaces are collectionwise normal; a metrizable space is collectionwise normal, so a non-collectionwise-normal Moore space is not metrizable (Moore spaces and developments, Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, Normalized families and collectionwise normality, Metrizable spaces are collectionwise normal, Discrete families and -locally-finite and -discrete bases).
Topological vocabulary: basis, open and closed sets, closure, discrete subspaces, subspace topology (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, Discrete families and -locally-finite and -discrete bases, Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly).
A function with domain and values in is exactly an element of ; finite sequences from are functions on natural numbers with range in ; the wood below is the set of all finite such sequences (A function is a relation with and implying ; , the value , domain and codomain, The natural numbers (von Neumann)).
Proof
Fix a well-ordering of the universe and enumerate the family as , arranged so that . Here with , and for ; write for the greatest ordinal in the range of a nonempty , and put and . Enumerating is legitimate: stationarity gives , so [F1] with gives ; and [F1] with gives at most subsets of size at most on every finite level. Conversely, the singletons of already give members of .
With , and the enumeration fixed as above, let be the least with ( for ), and for nonempty of length put . This set has cardinality at most . Using [F2], fix an enumeration with , arranged with ; the latter is possible because . Let and, for of length , define , with . Then : an element of has an index in , and cofinality of gives an with . Also, if and , then . Finally, has only finitely many nonempty prefixes, so , where if is infinite and if is finite. Thus the source's special clause gives finite ; it does not assert the false bound .
Construction requirement (well-definedness). The condition (12) below is imposed only at traces lying in : for , a triple satisfies (12) at index iff No instance of (12) is used anywhere below at a trace outside , and the §6 instances are proved in Case 1 below, so this guard is a definition of the space, not an assumption. This is the documented discharge of the trace-domain obligation.
Lemma 3(a). If satisfies , then for some the set has a stafull subset, where is stafull iff for all and the set is stationary in .
Let be the set of triples such that , for all , and is a function from to (for read ), and let . For let be the set of satisfying: or ; for all ; and the guarded (12) of step 1.3 at index . Put , and let with basis .
Suppose, for contradiction, that has no stafull subset for every ; then every nonempty is non-stafull, because a stafull subset of would be a stafull subset of . Call a finite acceptable iff for every and every nonempty with for all , there are and with such that is non-stationary. Then is acceptable by non-stafullness of itself. We construct whose every finite prefix is acceptable; then (else would be stafull) and for all , so , contradicting the covering hypothesis.
Lemma 3(b) in the form used. If is stafull and for a fixed , then there is a stafull on which is constant. Indeed is stationary, restricted to is regressive (ladder values are below their ordinal), so Fodor's lemma (F4) provides a stationary on which is constant; then is stafull: for the branching set equals the corresponding branching set of when (the first coordinate is determined by ) and equals when . Iterating for gives a stafull with for all and all .
Lemma 3(c). If is stafull and , then there is with iff or ( and ). Construct the coordinates level by level: having chosen levels so that all level- values lie below a common bound and each prefix extends to a member of , stafullness of makes each set stationary, hence unbounded above the bound; choose strictly increasing in and above the sup of the level- values, possible because that sup is by regularity (F1) since ; the final level's choice lies in by the definition of .
The family together with the singletons is a basis: for and the sequences are both initial segments of , hence comparable, and the longer one satisfies because : the conditions (10) and (11) transfer downwards, and a guarded (12)-instance at restricts to the corresponding instance at since by step 1.2 and for . For the singleton is a basis element contained in every basis element containing .
is , and is open, hence is closed. To see the property, distinct branches in have incompatible finite initial segments, while every has the open singleton . Conversely, for fixed and , choose ; then because condition (10) cannot make a length- sequence an initial segment of either length- coordinate. Thus every point other than has a neighbourhood avoiding , so is also closed.
Successor step of the acceptability recursion. Let be acceptable with . Call dangerous for if, for some , is nonempty, every extends , and is stationary for all and ; let some is dangerous for , and . Then .
The branch neighbourhoods have the star property needed below. If and open , choose with . For , the unique length- initial segment satisfies by step 3.1, so every length- basic member containing lies in . At a point of the singleton is a basic neighbourhood.
For disjoint closed , it is enough to find disjoint open with and . Indeed are open, contain respectively, and are disjoint: is discrete open, removing a closed set preserves openness, and each added isolated part lies in its own closed set and outside the other. Since is closed by step 3.2, the two traces are closed subsets of .
Suppose . If is stationary, choose for each the least level of a dangerous and a least such in the fixed well-order; some is stationary by the countable case split, and is nonempty with all members extending . Acceptability of gives and with non-stationary. Pick with . If then is stationary because is dangerous, a contradiction; if then , because witnesses for every , so is stationary, again a contradiction. If is non-stationary then is stationary and contained in , so is stationary; applying acceptability of to the nonempty and gives non-stationary for some , but is stationary. Both cases are contradictory, so .
Define . Each is an open cover: a point lies in , and every lies in its singleton. At , step 4.1 gives at every sufficiently large level. If , then for no with contains , because condition (10) would require to be an initial segment of one of the length- sequences ; thus . Moreover is a uniform base in the source's sense. A point belongs only to its singleton and to the finitely many whose is an initial segment of its two length- coordinates, so it cannot lie in the intersection of an infinite subfamily. If an infinite subfamily has , then has a branch , and the members of are the sets at arbitrarily large levels. Given open , choose with ; any member of with lies in . Hence is a neighbourhood base at . By the Aleksandrov-Arhangel'skij equivalence of uniform bases with metacompact Moore spaces recorded in the source's Section 2, is a regular Moore space and is metacompact.
Choosing gives that is acceptable — any nonempty above failing the acceptability witness would be dangerous for — and . The recursion produces an infinite sequence with every prefix acceptable and for all ; since means , the covering hypothesis is contradicted. Therefore some has a stafull subset, proving Lemma 3(a).
For and put and . It suffices to separate and by disjoint open subsets of for every (the source's Lemma 2). Here is the countable reduction. For disjoint closed , let Then and , because the cylinders are a base for . By the assumed -- separation, choose disjoint open containing , and disjoint open containing . Thus and , since the corresponding are open and disjoint. The open sets contain respectively and are disjoint: if a point lay in the th piece of and the th piece of , the case contradicts removal of from the latter, and contradicts removal of from the former. Step 4.2 then handles isolated points.
Non-metrizability. For put , a closed discrete family in . If were metrizable it would be collectionwise normal (F6), so there would be pairwise disjoint open sets .
Fix and with as in step 6.1, and let . Then is a club: it is closed because for a limit of -points and some has , so with ; and it is unbounded because the assignment can be iterated countably many times, remains below by regularity, and its limit lies in . This uses , so that at most distinct truncations occur, and .
Assume such exist. Put . Then : for one has , and since some basic neighbourhood lies in the open set ; then , so and , giving and with .
Let be the least element of greater than , and for choose where is the least with if , and otherwise; this is a definable choice from the given data. Then strictly, and whenever the transfer of step 1.2 gives (and even in , which is what the applications at index of level need). Put .
By Lemma 3(a) proved above there are and a stafull . Apply step 2.3 times to get a stafull with for all and , and apply step 2.4 with to obtain with the interleaving property. Put when and when . For , step 1.2 gives : nonemptiness follows from , , and . Enumerate it, repeating entries if necessary, as . Notice that is infinite when , while is finite when .
Claim (Case 1). Let and suppose , , and ; assume . Then .
For with , the triple for any satisfies (7), (8), (10), (11) of step 2.1: ; the interleaving of step 2.4 gives (8); gives (10); and (11) is exactly the constancy of from step 2.3. Since would put it into (as ), the guarded (12) must fail at index or at index for every .
Let : then there are , with , and , because and . By condition (10) at both indices the cases and and and force , so after interchanging and if necessary we have and ; hence , , and for , for .
Claim (Case 2). If under the hypotheses of step 9.1 (same membership assumptions), then .
For a fixed pair consider the two systems of constraints on , with the exponent always the triple's first component , and include only guarded instances whose trace lies in : the first system requires for of level , and the second requires the analogous value for . Each guarded system is internally consistent: by step 2.3 and , the required value depends only on the trace ; the same holds for the -system because by interleaving. No single total satisfies both guarded systems, by step 9.2. Hence a conflict exists: there are and whose common trace belongs to and for which but . Otherwise the function assigning each constrained trace its required value and to every other member of would satisfy both systems. This is (17) in trace form together with (18a) or (18b).
Condition (8) at the coordinates below and , together with step 10.1, gives . Before applying guarded (12), verify its domain condition. Since and are club points and , step 7.1 gives indices The Case-1 hypothesis gives , so both traces belong to . Step 8.1 now puts in and in . Their condition-(12) traces both reduce to because , while and . Thus guarded (12) yields , a contradiction. Hence Case 1 holds.
Assume and argue as in step 10.1 to get , ; then (8) gives the chain , so both and lie in the interval , which contains no -point by the minimality of ; applying the definition of inside that gap gives . By step 8.1, Put and ; then , and condition (11) at the indices , gives for every .
Define These sets are open and contain respectively: extend the length- initial segment of any branch to length and use . If Cases 1 and 2 both hold, every cross-pair of their displayed constituents is disjoint, according as or (interchange the two sequences first when their zeroth coordinates are reversed). Hence the two cases imply .
Colour each pair with by the least conflict witness in a fixed well-ordering of . If , this is a finite colour set and the infinite Ramsey theorem (F5) gives an infinite homogeneous set. If , then is infinite and, since , the Erdős–Rado theorem (F5) applied to a subset of of size gives a homogeneous set of size . Either way there are with and one common alternative of (18), common indices , and a common such that (17) holds for each of the three pairs.
The trace-domain verification in step 11.1 is symmetric for the two listed sets: their enumeration indices are below and , respectively, and both club successors lie below in Case 1. Thus every evaluation of made there is inside , as required by step 1.3.
Since (they are distinct elements of the interleaved family ) and both lie in , the ladder separation hypothesis applied at gives for every , in particular at . This contradicts the agreement of step 11.2 at level , because and . Hence Case 2 holds.
Step 11.1 proves Case 1 and step 12.2 proves Case 2, so step 11.3 gives disjoint open sets separating and for every and . The countable reduction of step 6.1 then separates arbitrary disjoint closed subsets of , and step 4.2 adds their isolated parts. Hence is normal.
With the triple of step 11.4 the printed chain computes: from (17) for the pairs , and the monotonicity from the interleaving, Under the common alternative (18a), the pair gives and the pair gives ; since by step 2.3, the chain transfers membership across and yields , a contradiction. Under (18b) the same two lines run with the membership signs exchanged. This contradiction establishes that is not disjoint, so is not collectionwise normal and hence not metrizable; with step 13.1 it is a normal nonmetrizable Moore space.
Remarks
- Two documented readings of the printed notation. (12) is used with the bound for a level- set, which is how the source's own Case 1 display on printed p. 370 uses it; the printed notation sentence after (12) is off by one restriction step. (17) is used in trace form , which is what the printed four-term chain displays. Both are recorded as local repairs, not source attributions.
- The two local repairs to the §6 parameters. is chosen strictly above the printed lower bounds, and the entry level of is arranged one step below ; without the strictness the printed Case 2 does not close. Recorded as a local repair.
- The trace-domain condition of step 1.3 is the guarded reading of (12); §6's instances are proved in step 12.1, and §7's instances are the applicable ones by definition, so no trace outside is ever evaluated.
- The finite-cardinal clause in (4). When , the source asks only that each be finite. Step 1.2 supplies the uniform finite bound , and step 11.4 uses that finite bound as the Ramsey colour set. No absorption identity is applied to a finite .
- AC is used in the enumeration of and of , in the choice of the ladders and the , in the countable recursion of step 3.3, and in the Ramsey/Erdős–Rado step; it is declared as a dependency and no choice-free reading is claimed.
Depends on
- Fleissner's HYP covering interface
- Cardinal (initial ordinal) and cardinality
- Cardinal sum $\kappa \oplus \lambda$, product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$, and why they are written apart from the ordinal operations
- Absorption: for cardinals $\kappa, \lambda$ with $\kappa$ infinite and $\lambda \le \kappa$, $\kappa \oplus \lambda = \kappa$, and $\kappa \otimes \lambda = \kappa$ when $\lambda \ne 0$
- Assuming the Axiom of Choice, $2^{\kappa} = \lvert \mathcal{P}(\kappa) \rvert$, and Cantor's theorem in cardinal form: $\kappa < 2^{\kappa}$
- Well-order and well-ordered set
- Injection, surjection, bijection
- The natural numbers $\mathbb{N}$ (von Neumann)
- A function is a relation $f$ with $(a,b) \in f$ and $(a,c) \in f$ implying $b = c$; $f : A \to B$, the value $f(a)$, domain and codomain
- Closed unbounded subsets of ordinals
- The club filter and nonstationary ideal
- Basic stationary-set calculus
- Fodor’s pressing-down lemma
- Regressive functions on ordinals
- The Axiom of Choice
- Erdős–Rado for arbitrary infinite cardinals and finite arity
- Infinite Ramsey theorem for fixed finite arity and colors
- Partition arrows and homogeneous sets
- Moore spaces and developments
- Regular spaces and $T_3$ spaces, with the source disagreement over whether regularity includes $T_1$ stated explicitly
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Normalized families and collectionwise normality
- Metrizable spaces are collectionwise normal
- Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not
- Discrete families and $\sigma$-locally-finite and $\sigma$-discrete bases
Used by
Dependency tree · two levels
104 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
- William G. Fleissner, If all normal Moore spaces are metrizable, then there is an inner model with a measurable cardinal (standard reference, not scraped)