Set.neg is preimage, but should be image

Stream: mathlib4

[Geoffrey Irving]

This is really splitting hairs, but I think the definition of Set.neg in Pointwise is slightly wrong. It is

/-- The pointwise inversion of set `s⁻¹` is defined as `{x | x⁻¹ ∈ s}` in locale `Pointwise`. It is
equal to `{x⁻¹ | x ∈ s}`, see `Set.image_inv`. -/
@[to_additive
      "The pointwise negation of set `-s` is defined as `{x | -x ∈ s}` in locale `Pointwise`.
      It is equal to `{-x | x ∈ s}`, see `Set.image_neg`."]
protected def inv [Inv α] : Inv (Set α) :=
  ⟨preimage Inv.inv⟩

but the documentation is wrong unless InvolutiveNeg: the documentation says image, but the definition is preimage. This doesn't matter to me in practice, but I hit it when I tried to define some downstream lemmas in full generality. I think the image definition is better, as it matches other definitions like Set.add.

Edit: Ah, the documentation does also say preimage, so arguably it's correct, though I still think the definition should be image.

[Geoffrey Irving]

(This isn't blocking me, since as with everyone else I have InvolutiveNeg in practice.)

[Johan Commelin]

I guess preimage has better defeqs. I don't know how much that matters...

[Geoffrey Irving]

The Neg / InvolutiveNeg advantage is minute, so if we want to exploit meaningful defeq wins those would win. Though mathematically the book definition is the one that works with Neg only.

[Eric Wieser]

There is an old thread about this at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/What.20should.20set.2Ehas_inv.20do.3F/near/271643067

[Yaël Dillies]

I originally argued for it to be preimage, but I since wrote an entire API based off the assumption it is image: file#Data/Set/NAry

[Geoffrey Irving]

It usually is! :)