New space: Product omega_1 x (omega_1 + 1) #1612
Conversation
There was a problem hiding this comment.
I think S218 should mentioned in the first line now. "I.e. S217 is the space S218 where we declary points in ... isolated". Thats sort of the point we (you) added it, no?
There was a problem hiding this comment.
Not sure. I thought of doing that, but it seemed useful to show the individual factors separately so that we have accessible links to them right at the top, instead of being hidden in the new S218. Adding mention of S218 at the end seemed fine to me.
There was a problem hiding this comment.
Should we maybe move the last line to be part of the first paragraph?
There was a problem hiding this comment.
Yeah, let me try that.
felixpernegger
left a comment
felixpernegger
left a comment
There was a problem hiding this comment.
Nice PR! just a few minor comments, then we can merge it I think
Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
…into omega1-omega1plus1
felixpernegger
left a comment
felixpernegger
left a comment
There was a problem hiding this comment.
Seems good now. Please merge if you dont have anything more to add :)
New space$\omega_1\times(\omega_1+1)$ .
See #1610.
Plus some meta-properties used here.
I also slightly modified S207 (Cohen's modification ...) to make use of the new space.