Zulip Chat Archive

Stream: condensed mathematics

Topic: by exactI


view this post on Zulip Floris van Doorn (Feb 06 2021 at 07:18):

I like that we have some notation for by exactI, but can we change it from a zero-width space to something more reasonable? We could use an English word that hasn't much meaning by itself, like now, so, thus? (though none of these quite sound right in the places we want)

view this post on Zulip Johan Commelin (Feb 06 2021 at 07:20):

If you can think of a fitting english word that is more reasonable than by exactI, I'm all for it.

view this post on Zulip Johan Commelin (Feb 06 2021 at 07:21):

Also, I think it's fine to just write by exactI almost everywhere.
I just wanted to avoid in the main statements, because there it's very distracting for outsiders that are reading their first lean code.

view this post on Zulip Johan Commelin (Feb 06 2021 at 08:16):

after the , of an \exists we could write such_that... but that doesn't fit very well after the , of \forall.
Of course we could have two new symbols.

view this post on Zulip Mario Carneiro (Feb 06 2021 at 08:24):

You could also write it such that you don't need by exactI...


Last updated: May 09 2021 at 23:10 UTC