## 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 now, so, 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):

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.

#### 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