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.
Balogh hereditary normality
Statement
Assume AC. In the Balogh space, any two separated subsets have disjoint open neighborhoods. Here separated means , with closures in the whole space. Consequently the space is hereditarily normal, Hausdorff and .
Facts & Assumptions
Given: The Balogh space and its levels and initial level unions .
Openness is witnessed by a finite family of binary equations at the immediately preceding level, with as defined in Balogh continuum topology.
These rules give a topology, each is open, and points on have neighborhoods contained in (Balogh neighborhood basis).
AC supplies simultaneous selections of the open separating neighborhoods whose existence is proved below (The Axiom of Choice).
Proof
For each and , we prove by finite induction that and have disjoint open neighborhoods contained in . For , use the two sets themselves, open by F1. At the successor stage let be the characteristic function of and put . The induction assertion gives disjoint open containing and its complement on . Adjoin to and its complement on to . At a new top point , the witness lies in if , and in its complement otherwise. F1 therefore makes the enlarged sets open; lower points already lie in the old opens. Disjointness holds on the new level and on the lower levels separately. This proves the assertion at every height.
We will use the following open-extension calculation. Suppose is closed, is open, and . For , put . At points of height at most , openness follows from . At a new point of height , the open set supplies by F1 a witness whose height- slice avoids , and this slice is contained in . At greater heights the same kind of witness lies above height and outside , hence inside the newly added part. Thus is open. The identical check at every finite height proves that is open as well. No claim that is closed was used.
Let be separated, and fix . Apply step 1.1 at level to the partition , . Obtain disjoint open containing those sets. Then contains . By step 1.2, is open; it contains because those points have height and avoid . Its newly added portion is outside , while ; the old portions are disjoint. Hence are disjoint open neighborhoods of these different-level subsets, both lying in .
Fix . For every choose such disjoint open about and . At level , step 1.1 supplies disjoint open about and . In particular these contain and . Put and . Both are open, disjoint, and respectively contain and . In addition by the choice of . Step 1.2 therefore makes open. It contains all of , because avoids , and remains disjoint from . Thus : each point of has the neighborhood avoiding . Repeating with interchanged yields open containing with . A1 permits fixing these choices for all . At the finite intersection contains only the same-level choice; no different-level choices are needed.
Define and . Each summand is open because only finitely many closed sets are removed. Every point of lies in some and in none of the , so ; likewise . If a point belonged to a -summand indexed by and a -summand indexed by , then would make the first omit , while would make the second omit . At least one comparison holds, including equality, so no such point exists. These are disjoint open neighborhoods of .
For any subspace and disjoint relatively closed , one has and , by the subspace closure definition. Thus are separated in . Step 4.1 gives disjoint open neighborhoods in , whose intersections with prove normality of . This also handles empty subsets and the empty subspace. F2 gives for ; apply its normality to two distinct closed singletons to get Hausdorff separation. Therefore all the asserted hereditary and separation properties hold. QED.
Depends on
Used by
Dependency tree · two levels
5 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.