Add results to show that pseudometrizable implies 1st countable by StevenClontz · Pull Request #244 · pi-base/data

StevenClontz · 2023-03-15T21:00:29Z

No description provided.

theorems/T000326.md

StevenClontz · 2023-03-15T21:37:49Z

This is obviously a very sketchy PR meant for tonight's demo purposes. I'll clean it up later this week I hope.

StevenClontz · 2023-03-16T00:45:22Z

Okay I think it's ready now.

ccaruvana · 2023-03-16T03:20:53Z

theorems/T000057.md

-If $X$ is pseudometric, for any $x \in X$, $\{B(x,\frac{1}{n})\,|\,n \in \omega\}$ is a countable local base at $x$.
-
-Asserted on page 34-35 of {{doi:10.1007/978-1-4612-6290-9}} for metric spaces.  The same holds for pseudometric spaces.
+Take a pseduometrizable neighborhood. The balls of rational radius within this neighborhood form a local basis.


I didn't catch this before accepting the pull request, but "pseudometrizable" is misspelled; it appears as "pseduometrizable"

I'll make a hotfix for this directly on main.

I'll make a hotfix for this directly on main.

Seems T327 has the same missplelling.

Fixed now in 70e67cd. I'm okay if maintainers/reviewers do trivial (literally one line) typo changes directly on main.

Go to e.g. https://github.com/pi-base/data/blob/main/theorems/T000327.md click the pencil icon to get a quick editor, make the fix, change the commit message to say "fixed typo" (I forgot to do this at 70e67cd), then commit directly to main.

Not sure it would let me do this. Just to check, I clicked on the pencil icon and at the bottom it says "you can't commit to main, because it's a protected branch. Create a new branch for this commit and start a pull request."

Oops. I guess that might be an admin-only feature. So in that case I still recommend the workflow when convenient, but rather than committing to main, create a "patch" branch and open a PR that can be quickly reviewed/accepted by others.

prabau · 2023-03-16T04:30:45Z

Nice.

I was looking at the new https://topology.pi-base.org/theorems/T000327 (loc metrizable ==> loc pseudometrizable) in pi-base and wondering why there is currently no example showing the converse is not true. The indiscrete topology on two points should be one automatically.

I think loc metrizable should automatically imply T1. Loc metrizable implies locally T1, and a space that is locally T1 should be T1, if my reasoning is not mistaken. Does this last implication seem correct to you guys? If it's correct and not entirely obvious, we could add/answer a question on mathse and then add [loc metrizable ==> T1]?

prabau · 2023-03-16T04:43:57Z

Found this: https://math.stackexchange.com/questions/3142975

So indeed, locally T1 implies T1. I can add [locally metrizable ==> T1] (T2 would be too strong, as shown by the telophase topology (S65). By the same token we can also add [locally Euclidean ==> locally metrizable], and the same S65 is in fact locally Euclidean.

(Added later) S65 (telophase topology) is not locally Euclidean at the endpoints. The "line with two origins" (which pi-base does not have) is really a similar thing and would be locally Euclidean.

StevenClontz · 2023-03-16T16:20:46Z

Sounds like a good addition @prabau.

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net>

prabau · 2023-03-17T17:21:12Z

Oops. I guess that might be an admin-only feature. So in that case I still recommend the workflow when convenient, but rather than committing to main, create a "patch" branch and open a PR that can be quickly reviewed/accepted by others.

Actually it's possibly a permission problem. For example, when I have approved a PR, it never gives me the option to merge afterwards. But I think Chris can merge without problem.

@ccaruvana Can you try to see if doing a one line change directly on the main allows you to commit immediately to main?

StevenClontz · 2023-03-17T17:24:47Z

I think you're right @prabau - I've given you maintainer permissions now.

prabau · 2023-03-17T17:29:31Z

I tried again to commit a change directly to main, but same as before. Maybe the change takes a little bit of time to take effect. I have to be away from my desk now, will try again later.

prabau · 2023-03-17T20:08:15Z

Seems it makes no difference. So creating a patch branch is the way to go then.

ccaruvana · 2023-03-17T22:37:40Z

@prabau and @StevenClontz Sorry I'm late to the party. Even though it seems this all has been resolved, I wanted to follow through with the request. So I tried a push directly to main and got this error message: "You are trying to commit to a protected branch and you do not have permission to push your commits to the remote." I'm assuming this is the issue that Patrick was having.

prabau · 2023-03-17T22:40:16Z

@prabau and @StevenClontz Sorry I'm late to the party. Even though it seems this all has been resolved, I wanted to follow through with the request. So I tried a push directly to main and got this error message: "You are trying to commit to a protected branch and you do not have permission to push your commits to the remote." I'm assuming this is the issue that Patrick was having.

Yes, that's what I was observing too.

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * Update CITATION.cff (#260) * T209 generalization (#264) * T209 generalization * fix typo * T208: indiscrete + distinct points ==> no isolated point (#266) * S27 and S28 updates (#261) * S27 updates * S28 updates * fix typo * S27/P23: added reference * S31: square of one point compactification of Q (#263) --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * Update CITATION.cff (#260) * T209 generalization (#264) * T209 generalization * fix typo * T208: indiscrete + distinct points ==> no isolated point (#266) * S27 and S28 updates (#261) * S27 updates * S28 updates * fix typo * S27/P23: added reference * S31: square of one point compactification of Q (#263) * S153: Open long ray (#270) * S153: Open long ray * improve lindelof->weakly lindelof --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * split up theorems implying conjunctions of properties (#267) * split up theorems implying conjuctions of properties * remove proposed but out-of-syntax deprecatedBy * Update T000042.md * Update T000099.md * Update T000100.md * add converse * Delete T000171.md * Update T000176.md * Update T001042.md * Update T001176.md * fix typos * split T104 * fix uid * consolidate theorem IDs * add a few converses --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * more inclusive choice of default terminology (#271) * more inclusive choice of default terminology * Update README.md * Update README.md * Update README.md --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * Update CITATION.cff (#260) * T209 generalization (#264) * T209 generalization * fix typo * T208: indiscrete + distinct points ==> no isolated point (#266) * S27 and S28 updates (#261) * S27 updates * S28 updates * fix typo * S27/P23: added reference * S31: square of one point compactification of Q (#263) * S153: Open long ray (#270) * S153: Open long ray * improve lindelof->weakly lindelof --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * split up theorems implying conjunctions of properties (#267) * split up theorems implying conjuctions of properties * remove proposed but out-of-syntax deprecatedBy * Update T000042.md * Update T000099.md * Update T000100.md * add converse * Delete T000171.md * Update T000176.md * Update T001042.md * Update T001176.md * fix typos * split T104 * fix uid * consolidate theorem IDs * add a few converses --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * more inclusive choice of default terminology (#271) * more inclusive choice of default terminology * Update README.md * Update README.md * Update README.md * add sequential property to arens space (#274) * T82: locally euclidean => locally arc connected (#272) * connect rothberger property and create counterexamples (#275) * Update P000144.md * Fix P144 line ending * fix MR refs * Fix more MR refs * add aliases for separation properties (#276) * improve regular to t3 (#277) * improve regular to t3 * improve t3 to t3.5 for S77 (and add t5 for P63) * add michael line S63 normality props * swap the factors to map S&S --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * Update CITATION.cff (#260) * T209 generalization (#264) * T209 generalization * fix typo * T208: indiscrete + distinct points ==> no isolated point (#266) * S27 and S28 updates (#261) * S27 updates * S28 updates * fix typo * S27/P23: added reference * S31: square of one point compactification of Q (#263) * S153: Open long ray (#270) * S153: Open long ray * improve lindelof->weakly lindelof --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * split up theorems implying conjunctions of properties (#267) * split up theorems implying conjuctions of properties * remove proposed but out-of-syntax deprecatedBy * Update T000042.md * Update T000099.md * Update T000100.md * add converse * Delete T000171.md * Update T000176.md * Update T001042.md * Update T001176.md * fix typos * split T104 * fix uid * consolidate theorem IDs * add a few converses --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * more inclusive choice of default terminology (#271) * more inclusive choice of default terminology * Update README.md * Update README.md * Update README.md * add sequential property to arens space (#274) * T82: locally euclidean => locally arc connected (#272) * connect rothberger property and create counterexamples (#275) * Update P000144.md * Fix P144 line ending * fix MR refs * Fix more MR refs * add aliases for separation properties (#276) * improve regular to t3 (#277) * improve regular to t3 * improve t3 to t3.5 for S77 (and add t5 for P63) * add michael line S63 normality props * swap the factors to map S&S --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * add counterexample from https://math.stackexchange.com/q/3145712 (#279) * add counterexample * Update README.md * remove T0 assumption in T23 (#283) * remove T0 assumption in T23 * actually update T23 * Update T000023.md --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * Update CITATION.cff (#260) * T209 generalization (#264) * T209 generalization * fix typo * T208: indiscrete + distinct points ==> no isolated point (#266) * S27 and S28 updates (#261) * S27 updates * S28 updates * fix typo * S27/P23: added reference * S31: square of one point compactification of Q (#263) * S153: Open long ray (#270) * S153: Open long ray * improve lindelof->weakly lindelof --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * split up theorems implying conjunctions of properties (#267) * split up theorems implying conjuctions of properties * remove proposed but out-of-syntax deprecatedBy * Update T000042.md * Update T000099.md * Update T000100.md * add converse * Delete T000171.md * Update T000176.md * Update T001042.md * Update T001176.md * fix typos * split T104 * fix uid * consolidate theorem IDs * add a few converses --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * more inclusive choice of default terminology (#271) * more inclusive choice of default terminology * Update README.md * Update README.md * Update README.md * add sequential property to arens space (#274) * T82: locally euclidean => locally arc connected (#272) * connect rothberger property and create counterexamples (#275) * Update P000144.md * Fix P144 line ending * fix MR refs * Fix more MR refs * add aliases for separation properties (#276) * improve regular to t3 (#277) * improve regular to t3 * improve t3 to t3.5 for S77 (and add t5 for P63) * add michael line S63 normality props * swap the factors to map S&S --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * add counterexample from https://math.stackexchange.com/q/3145712 (#279) * add counterexample * Update README.md * remove T0 assumption in T23 (#283) * remove T0 assumption in T23 * actually update T23 * Update T000023.md * add paracompact properties and arens space props (#282) * add paracompact properites and arens space props * Update P000050.md * Update P000146.md * misc changes * add alternate def for ultraparacompact --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * Some more properties for the Arens space (#285) * More Arens space updates * fix for scattered property --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * Update CITATION.cff (#260) * T209 generalization (#264) * T209 generalization * fix typo * T208: indiscrete + distinct points ==> no isolated point (#266) * S27 and S28 updates (#261) * S27 updates * S28 updates * fix typo * S27/P23: added reference * S31: square of one point compactification of Q (#263) * S153: Open long ray (#270) * S153: Open long ray * improve lindelof->weakly lindelof --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * split up theorems implying conjunctions of properties (#267) * split up theorems implying conjuctions of properties * remove proposed but out-of-syntax deprecatedBy * Update T000042.md * Update T000099.md * Update T000100.md * add converse * Delete T000171.md * Update T000176.md * Update T001042.md * Update T001176.md * fix typos * split T104 * fix uid * consolidate theorem IDs * add a few converses --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * more inclusive choice of default terminology (#271) * more inclusive choice of default terminology * Update README.md * Update README.md * Update README.md * add sequential property to arens space (#274) * T82: locally euclidean => locally arc connected (#272) * connect rothberger property and create counterexamples (#275) * Update P000144.md * Fix P144 line ending * fix MR refs * Fix more MR refs * add aliases for separation properties (#276) * improve regular to t3 (#277) * improve regular to t3 * improve t3 to t3.5 for S77 (and add t5 for P63) * add michael line S63 normality props * swap the factors to map S&S --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * add counterexample from https://math.stackexchange.com/q/3145712 (#279) * add counterexample * Update README.md * remove T0 assumption in T23 (#283) * remove T0 assumption in T23 * actually update T23 * Update T000023.md * add paracompact properties and arens space props (#282) * add paracompact properites and arens space props * Update P000050.md * Update P000146.md * misc changes * add alternate def for ultraparacompact --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * Some more properties for the Arens space (#285) * More Arens space updates * fix for scattered property * Fix for Fully normal (P34) (#289) * Fix for Fully normal (P34) * add one reference * generalize T214 from fully T4 to fully normal (#288) --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

* fix line ending issues * fix: add ref name to mathse ref See pi-base/web#10 * Update CONTRIBUTING.md * Weak Hausdorff property (#237) * Weak Hausdorff property * Add properties for weak Hausdorff * T227: tweak the explanation * add kspace properties and theorems (#236) * add kspace properites and theorems * tweaking the definitions * Update P000141.md * Update P000140.md --------- Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> * S37: example of US, non weak Hausdorff space (#241) * Fix typo in P84 * Add results to show that pseudometrizable implies 1st countable (#244) * Add results to show that pseudometrizable implies 1st countable * fix T327 id * fix typos in P144 * add mathse reference * Fix typo * Update T000327.md * Some theorems and traits involving local metrizability (#248) * More theorems about locally pseudometrizable (#250) * More theorems about locally pseudometrizable * T331 converse * Misc spaces: more precise position between T1 and T2 (#249) * Misc spaces: more precise position between T1 and T2 * remove unneeded T2 assertion * remove another unneeded T2 assumption --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T328 update (#252) * Included locally Euclidean -> locally compact to get some examples of spaces which are locally metrizable but not locally Euclidean. * fixed parse error * fixed another typo * suggested edits * Use citation cff (#253) * Commit line-ending changes auto-enforced by git * Adds a CITATION.cff file to make use of the github citation button feature https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files * Update CITATION.cff --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * T230: first countable + US imply T2 (#257) * T230: first countable + US imply T2 * remove deduceable T1 --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * Update CITATION.cff (#260) * T209 generalization (#264) * T209 generalization * fix typo * T208: indiscrete + distinct points ==> no isolated point (#266) * S27 and S28 updates (#261) * S27 updates * S28 updates * fix typo * S27/P23: added reference * S31: square of one point compactification of Q (#263) * S153: Open long ray (#270) * S153: Open long ray * improve lindelof->weakly lindelof --------- Co-authored-by: Steven Clontz <steven.clontz@gmail.com> * split up theorems implying conjunctions of properties (#267) * split up theorems implying conjuctions of properties * remove proposed but out-of-syntax deprecatedBy * Update T000042.md * Update T000099.md * Update T000100.md * add converse * Delete T000171.md * Update T000176.md * Update T001042.md * Update T001176.md * fix typos * split T104 * fix uid * consolidate theorem IDs * add a few converses --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * more inclusive choice of default terminology (#271) * more inclusive choice of default terminology * Update README.md * Update README.md * Update README.md * add sequential property to arens space (#274) * T82: locally euclidean => locally arc connected (#272) * connect rothberger property and create counterexamples (#275) * Update P000144.md * Fix P144 line ending * fix MR refs * Fix more MR refs * add aliases for separation properties (#276) * improve regular to t3 (#277) * improve regular to t3 * improve t3 to t3.5 for S77 (and add t5 for P63) * add michael line S63 normality props * swap the factors to map S&S --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * add counterexample from https://math.stackexchange.com/q/3145712 (#279) * add counterexample * Update README.md * remove T0 assumption in T23 (#283) * remove T0 assumption in T23 * actually update T23 * Update T000023.md * add paracompact properties and arens space props (#282) * add paracompact properites and arens space props * Update P000050.md * Update P000146.md * misc changes * add alternate def for ultraparacompact --------- Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> * Some more properties for the Arens space (#285) * More Arens space updates * fix for scattered property * Fix for Fully normal (P34) (#289) * Fix for Fully normal (P34) * add one reference * generalize T214 from fully T4 to fully normal (#288) * Add a perfectly normal, non fully normal space (#287) * add perfectly normal non fully normal space * Update README.md * Updates to Fortissimo space (S22) (#292) * Some theorems involving compactly generated (#290) * Some theorems involving compactly generated * Example of space with P140 and not P141 * T70 to provide spaces with P141 and not P142 * Better version of T70 * change the ref for T70 * Convenience aliases for compactly generated (#293) * Updates to Single ultrafilter topology (#294) --------- Co-authored-by: James Dabbs <james.dabbs@gmail.com> Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> Co-authored-by: Patrick Rabau <prabau@sbcglobal.net> Co-authored-by: Chris <30360237+ccaruvana@users.noreply.github.com> Co-authored-by: rschwiebert <rschwiebert@users.noreply.github.com>

StevenClontz added 2 commits March 15, 2023 15:59

Add results to show that pseudometrizable implies 1st countable

0f1a0ff

fix T327 id

c59a23b

StevenClontz requested a review from ccaruvana March 15, 2023 21:01

StevenClontz commented Mar 15, 2023

View reviewed changes

theorems/T000326.md Show resolved Hide resolved

fix typos in P144

1672e64

add mathse reference

7ca0fea

ccaruvana approved these changes Mar 16, 2023

View reviewed changes

ccaruvana merged commit 44976b1 into main Mar 16, 2023

ccaruvana deleted the stdc-demo branch March 16, 2023 03:07

ccaruvana reviewed Mar 16, 2023

View reviewed changes

prabau mentioned this pull request Mar 17, 2023

Some theorems and traits involving local metrizability #248

Merged

prabau mentioned this pull request Mar 21, 2023

Use citation cff #253

Merged

Comments

Conversation

StevenClontz commented Mar 15, 2023

Uh oh!

Uh oh!

StevenClontz commented Mar 15, 2023

Uh oh!

StevenClontz commented Mar 16, 2023

Uh oh!

ccaruvana Mar 16, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

StevenClontz Mar 16, 2023

Choose a reason for hiding this comment

Uh oh!

prabau Mar 16, 2023

Choose a reason for hiding this comment

Uh oh!

StevenClontz Mar 16, 2023

Choose a reason for hiding this comment

Uh oh!

prabau Mar 16, 2023

Choose a reason for hiding this comment

Uh oh!

StevenClontz Mar 17, 2023

Choose a reason for hiding this comment

Uh oh!

prabau commented Mar 16, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

prabau commented Mar 16, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

StevenClontz commented Mar 16, 2023

Uh oh!

prabau commented Mar 17, 2023

Uh oh!

StevenClontz commented Mar 17, 2023

Uh oh!

prabau commented Mar 17, 2023

Uh oh!

prabau commented Mar 17, 2023

Uh oh!

ccaruvana commented Mar 17, 2023

Uh oh!

prabau commented Mar 17, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ccaruvana Mar 16, 2023 •

edited

Loading

prabau commented Mar 16, 2023 •

edited

Loading

prabau commented Mar 16, 2023 •

edited

Loading