by exactI

Stream: condensed mathematics

[Floris van Doorn]

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]

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

[Johan Commelin]

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]

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]

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