Stream: condensed mathematics
Topic: by exactI
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
thus? (though none of these quite sound right in the places we want)
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.
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.
Johan Commelin (Feb 06 2021 at 08:16):
, of an
\exists we could write
such_that... but that doesn't fit very well after the
Of course we could have two new symbols.
Mario Carneiro (Feb 06 2021 at 08:24):
You could also write it such that you don't need
Last updated: May 09 2021 at 23:10 UTC