My pet peeve with negation

Stream: lean4

[Martin Dvořák]

I have a per peeve with negation.
We write neither parentheses nor spaces around the (prefix) negation operator.
It can look like this:

¬A ⊂ B

From technical perspective, there is nothing wrong with it; it is unambiguous and concise.
Unfortunately, it confuses my brain.
I almost never read it correctly on the first try.
To me, it looks like "some operation applied to A gives a strict subset of B".
Am I the only one?
Do we want to change it?
Two possible alternatives are:

¬ A ⊂ B
¬(A ⊂ B)

Changing it would mean both changing the declaration of the notation or its delaborator, and refactoring Std and Mathlib to the new convention.

[Edward van de Meent]

perhaps we should just use ⊄ for this?

[Martin Dvořák]

I don't think we should create a crossed version of all infix operators.

[Edward van de Meent]

does that also restrict to those with result type Bool or Prop? (in typical use case)

[Martin Dvořák]

Do you want to suggest that we should create a negated version for all relational infix operators?
I think @Kevin Buzzard had a similar suggestion in the past.

[Kevin Buzzard]

i don't remember having an issue with negation in general but I do remember having a pet peeve with ¬ x ∈ S years ago and the upshot being that we now have x ∉ S

[Edward van de Meent]

possibly... ideally, these are just notation/pretty print things i think (e.g. i don't like how ≠ gets simped to ¬A = B (or why these even are separate things))

[Edward van de Meent]

even if we are not going to add this new symbol, i do agree that ¬A ⊂ B is too easily read (¬A) ⊂ B, and indeed prefer ¬(A ⊂ B)

[Edward van de Meent]

similar for ⊆, all those other set notations

[Jireh Loreaux]

Martin Dvořák said:

We write neither parentheses nor spaces around the (prefix) negation operator.

I don't understand. We can? These parse fine:

example (R : Type*) {s t : Set R} : ¬ s ⊂ t := sorry
example (R : Type*) {s t : Set R} : ¬(s ⊂ t) := sorry

[Jireh Loreaux]

I think if you want to do this, then go for it. If a reviewer complains then have the Zulip discussion.

[Eric Wieser]

I suspect that Martin meant to complain that "the infoview writes neither [...]"

[Edward van de Meent]

I think that the appropriate binding strength might be something at about arg-ε