Theory Meeting, Dec. 12th

Ed Snow

unread,

Dec 12, 2018, 2:41:02 PM12/12/18

to pdxfunc

For tonight's meeting I've completed proofs (sorry-free this time) for the reflexivity, transitivity, antisymmetry, and totality of ≤ as discussed in Section 17.5:

https://gist.github.com/es30/13081dced39df89ff83f20bf20b3494f

Matt Rice

unread,

Dec 12, 2018, 3:13:43 PM12/12/18

to pdx...@googlegroups.com

On Wed, Dec 12, 2018 at 11:41 AM Ed Snow <edsn...@gmail.com> wrote:
>
> For tonight's meeting I've completed proofs (sorry-free this time) for the reflexivity, transitivity, antisymmetry, and totality of ≤ as discussed in Section 17.5:
>
> https://gist.github.com/es30/13081dced39df89ff83f20bf20b3494f

Nice, your antisymmetry proof turned out way nicer than mine did,
where I managed to miss add_zero/cancellation and wound up bottoming
out at n + ... \neq succ n + ...
I managed to get through quite a few, up to trichotomy. Except the
multiplication ones, which I could not figure out.

https://gist.github.com/ratmice/7df331c34ed5abfe6fe5e9d1c3d83636

Lyle Kopnicky

unread,

Dec 16, 2018, 7:07:26 PM12/16/18

to pdxfunc

Thanks to you both, it was really interesting seeing your solutions.

On Wednesday, December 12, 2018 at 12:13:43 PM UTC-8, Matt Rice wrote:

Reply all

Reply to author

Forward