New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. Weβll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Define the indiscrete topology in iset.mm #3089
Comments
I think you can also do similar things for the other topologies mentioned in #3088:
|
I'll ask my usual question: Should we modify the definition in set.mm so it would work in both set.mm and iset.mm? I suspect the answer may be "no" in this case, but I feel I should ask. |
This sentence is not very clear and does not match the statement. I think a more transparent expression for the indiscrete topology on
where the restricted nonfreeness quantifier has the natural definition |
I think it's a bit much to add a restricted not-free quantifier just for that. FTR I got that definition by starting from |
Yes, it wouldn't make sense to define the restricted nonfreeness quantifier just for that, but I think it's missing anyway (A., E., E!, E*, _iota, { | }, all have their restricted versions), so we might as well use it here once it's introduced. Without using the nonfreeness quantifier, this would give |
My usual answer is that we shouldn't do so if the modified definition would be significantly longer or more awkward, and this feels like such a situation to me. If you have excluded middle it is really odd to have to explain what's wrong with |
Fair enough, I suspected that but I felt I had to ask. |
The definition in set.mm - in https://us.metamath.org/mpeuni/indistopon.html and related theorems - is {β , π΄} and that is not going to work intuitionistically.
We plan on defining it to be the collection of all sets such that the membership relation does not depend on
x
, i.e.{ s | A. x e. s s = X }
The key theorems are the analogues to https://us.metamath.org/mpeuni/indistopon.html , https://us.metamath.org/mpeuni/indistop.html , https://us.metamath.org/mpeuni/indisuni.html , https://us.metamath.org/mpeuni/indistps.html , https://us.metamath.org/mpeuni/indistps2.html . There are a few more which depend on those, but that's the start.
The text was updated successfully, but these errors were encountered: