Timeline for Strictly-monotone "max" operation for constructive Brouwer-trees?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 6, 2022 at 22:16 | comment | added | Joey Eremondi | Ohhhh, I see. Hmm, I'll try that. | |
| Jun 6, 2022 at 21:20 | comment | added | Dan Doel | It's not lexicographic. It's a 'partial order' where $p < q$ means one side of $p$ is less than the corresponding side of $q$, and the opposite side is same. There could be a constructor where both are less, as well, which would fill in transitivity gaps. So, on every step one side gets smaller, and neither side ever gets bigger. I don't know if that actually describes your function, though. | |
| Jun 6, 2022 at 21:02 | comment | added | Joey Eremondi | "(just a lot of cases)" - Yeah, this may be where I got stuck. I was assuming that the explosion meant I was doing something wrong, but I wasn't actually able to come up with a counter-example. For the ⊕ operator, that's lexicographic ordering, right? | |
| Jun 3, 2022 at 7:31 | history | edited | Dan Doel | CC BY-SA 4.0 |
added 790 characters in body
|
| Jun 3, 2022 at 3:46 | history | answered | Dan Doel | CC BY-SA 4.0 |