Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions properties/P000243.md
Comment thread
felixpernegger marked this conversation as resolved.
Original file line number Diff line number Diff line change
Expand Up @@ -20,3 +20,6 @@ Defined on page 14 of {{zb:0559.54003}}.
#### Meta-properties

- This property is hereditary with respect to dense sets.
- This property is hereditary with respect to open sets.
- $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does.
- This property is preserved by countable products.
3 changes: 3 additions & 0 deletions properties/P000244.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,3 +23,6 @@ Defined on page 16 of {{zb:0559.54003}}.
#### Meta-properties

- This property is hereditary with respect to dense sets.
- This property is hereditary with respect to open sets.
- $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does.
- This property is preserved by countable products.
7 changes: 7 additions & 0 deletions spaces/S000108/properties/P000243.md
Comment thread
felixpernegger marked this conversation as resolved.
Comment thread
felixpernegger marked this conversation as resolved.
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
---
space: S000108
property: P000243
value: true
---

The set $\{\{n\}: n < \omega\}$ is a countable $\pi$-base for $\beta \omega$.
7 changes: 7 additions & 0 deletions spaces/S000111/properties/P000243.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
---
space: S000111
property: P000243
value: true
---

$X$ is a dense subspace of {S108} and {S108|P243}.
7 changes: 7 additions & 0 deletions spaces/S000216/properties/P000243.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
---
space: S000216
property: P000243
value: true
---

$X$ is a dense subspace of {S108} and {S108|P243}.
15 changes: 13 additions & 2 deletions theorems/T000902.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,20 @@
---
uid: T000902
if:
P000027: true
and:
- P000244: true
- P000026: true
then:
P000243: true
refs:
- zb: "0559.54003"
name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology
---

A base for the topology is a $\pi$-base.
Let $A$ be a countable dense subset of $X$.
For each $x\in A$, let $\mathcal V_x$ be a countable local $\pi$-base for $x$.
Then $\bigcup\{\mathcal V_x:x\in A\}$ is a countable (global) $\pi$-base.

To see this, if $O$ is a nonempty open set, there is some $x\in A\cap O$. Hence $O$ contains some $V\in\mathcal V_x$.

This is a special case of Theorem 3.8(b) of {{zb:0559.54003}}.
16 changes: 16 additions & 0 deletions theorems/T000903.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
---
uid: T000903
if:
and:
- P000011: true

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
- P000011: true
- P000005: true

This stays closed to the source; this doesnt weaken the assumption since regular + has point g delta => t3 anyways

@prabau prabau May 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@JSMassmann Please change P5 to P11. It is equivalent since (points G_delta) implies T1. If you compare the theorem pages for each of the properties (https://topology.pi-base.org/properties/P000011 vs. https://topology.pi-base.org/properties/P000005), when we can phrase a theorem with just regular in the hypotheses, we do so, as it is a formally weaker property. In the general case, technically it's very very slightly easier to check the hypotheses, and the theorem has wider applicability. (of course equivalent in this case) But, more that that, using regular here allows to have the theorem side by side with other theorems that also use "regular + points G_delta" in the hypotheses, like T508.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The source explicitly write T3 and not regular. Writing anything else complicates this for no reason.

I am strongly against this.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the general case, technically it's very very slightly easier to check the hypotheses and the theorem thus has wider applicability. (of course equivalent in this case) But, more that that, using regular here allows to have the theorem side by side with other theorems that also use "regular + points G_delta" in the hypotheses, like T508.

Most (or at least a lot of) theorems in pibase are essentially unusable directly anyways
(For example we do not have urysohn metrization theorem lol).

Instead deduction engine works very well

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@felixpernegger You keep insisting about following the source. You did the same in other PRs. This is misguided. Often we modify things to best fit what we want to present in pi-base. It does not really matter what one source says. It's just one tool in the justification of a result. (For another example, many sources make blanket assumptions of some separation axioms. Engelking for example in many places. But we don't add the same assumption if it's not needed.)

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We obviously should have theorems in their most general form, but dont abuse sources.
A good example/practise of this is https://topology.pi-base.org/theorems/T000845

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@felixpernegger Since things are equivalent, and like you said, the deduction engine works very well, you should not have a problem with either choice. And since for some people it is helpful to have things presented in a certain way, it should hopefully not matter to you.

The individual need to be perfectly clear. It is fine to just use outside sources obv, but if we say something is Corollary XY and then the result is actually not, we need to clarify this. A more glarring example is the other suggestion I made to the pr

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A more glarring example is the other suggestion I made to the pr

I totally agree about that one. I thought yesterday about making a suggestion along these lines and you beat me to it. (Actually I wanted to suggest something a little more explicit. Will write it up.)

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So... what should it be? P5 or P11? I personally don't mind, I see the arguments for both.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So... what should it be? P5 or P11? I personally don't mind, I see the arguments for both.

I think its best if you decide.

- P000029: true
- P000191: true
- P000244: true
then:
P000163: true
refs:
- zb: "0559.54003"
name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology
---

See Corollary 6.4 of {{zb:0559.54003}}.
19 changes: 19 additions & 0 deletions theorems/T000904.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
---
uid: T000904
if:
and:
- P000087: true
- P000244: true
then:
P000028: true
---

Because {T347}, it suffices to check the identity element $e$ has a countable local base.
Let $\mathcal{U}$ be a countable local $\pi$-base around $e$.
Put $\mathcal{W} = \{U \cdot U^{-1}: U \in \mathcal{U}\}$.

We claim $\mathcal{W}$ is a countable local base around $e$.
Every element of $\mathcal{W}$ is an open neighbourhood of $e$.
And if $V$ is a neighbourhood of $e$, there is an open neighbourhood $O$ of $e$ such that $O\cdot O^{-1}\subseteq V$ by continuity of the group operations.
By hypothesis, $O$ contains some $U \in \mathcal{U}$.
Then $U \cdot U^{-1} \subseteq V$.
16 changes: 16 additions & 0 deletions theorems/T000905.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
---
uid: T000905
if:
and:
- P000134: true
- P000016: true
- P000081: true
then:
P000244: true
refs:
- zb: "0559.54003"
name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology
---

The result with {P134} replaced by {P3} is a special case of Theorem 7.13 in {{zb:0559.54003}} (which uses "compact" to mean compact Hausdorff).
The current result is obtained by passing to the Kolmogorov quotient.
Loading