compactness example

[greleigh]

Removed \div from function symbols on rationals (it’s not total and not needed).

[rzach]

Um, we do need it for this example! (we could say c \times k < 1 instead of c < 1 \div k but I think that would make it less clear what's going on)

[greleigh]

There is the issue that the interpretation of \div is not total. If kept, qualification of the “obvious interpretation” of \div is probably needed.

I’ve added a commit removing the remaining uses of \div in the example.

[beastaugh]

I've created an alternative pull request that tries to keep the intuitive quality of having division in the language but removing it from the official signature.

I don't have a strong preference between this and @greleigh's more minimal approach, but I think it should be changed to remove the division symbol from the official signature.

[rzach]

I think I like this a bit better than @beastaugh 's proposal since it avoids introducing a definition. But I thought it could stand to have a tiny bit of explanation of how it works (ie pointing out that r < 1/k iff rk < 1). What do you think?

[beastaugh]

This looks good to me.

[greleigh]

I agree

[rzach]

Thanks to both of you!