Set.forall_image_iff

Stream: Is there code for X?

[Geoffrey Irving]

We have Finset.forall_image and Set.forall_image2_iff, so I'm surprised that I can't find Set.forall_image_iff. Is that because it's handlable with other simps? It would be

theorem Set.forall_image_iff {α β : Type*} {f : α → β} {s : Set α} {p : β → Prop} : (∀ y ∈ f '' s, p y) ↔ ∀ x ∈ s, p (f x) := by
  sorry

[Notification Bot]

Geoffrey Irving has marked this topic as resolved.

[Notification Bot]

Geoffrey Irving has marked this topic as unresolved.

[Yaël Dillies]

docs#Set.ball_image_iff

[Yaël Dillies]

One of the all-time winners for worst lemma name

[Geoffrey Irving]

Thanks. Yes, it didn't occur to me to search for ball.

[Yaël Dillies]

Actually I'm really annoyed by this name (and have been for a long time) and I have five minutes. Let me open a PR.

[Geoffrey Irving]

Thank you!

[Eric Rodriguez]

Can't we just add lots of aliases instead of deleting lemma names?

[Eric Rodriguez]

I don't see why every lemma has to have a unique name

[Yaël Dillies]

Yeah but Set.mem_ball_iff really is just a bad name

[Jireh Loreaux]

What did you change it to?

[Yaël Dillies]

I'm going to change it to Set.forall_mem_image

[Yaël Dillies]

#10816

[Sébastien Gouëzel]

Looks good (modulo the linting), thanks! I'd like a second opinion before borsing it, though, because these names have been here for so long that there may be a reason.

[Yaël Dillies]

Feel free to push fixes. I need to work for the next few hours.

[Eric Rodriguez]

I agree that this name was especially bad. I do think we should err against fully changing names in future as opposed to just adding aliases

[Yaël Dillies]

I don't understand your stance. Most lemma names are clear improvements. It's quite rare that a lemma has several valid names

[Eric Rodriguez]

I can think of many. Plus, names are cheap - why do we care so much if people choose the wrong one? I think this can only be a positive to discoverability (with the caveat that maybe tools like Loogle need to handle aliases especially; not sure if they do already)

[Geoffrey Irving]

I think a norm of leaving old names in place with a comment pointing to the new one would be great. But I agree this would be a shift in mathlib policy.

[Michael Stoll]

One can add the old name as a deprecated alias (to help migration downstream).

[Eric Rodriguez]

But I'm not sure why it needs to be deprecates. There is zero maintenance overhead to keeping names around. I'd favour deprecating maybe particularly bad names like this one, but in general I don't know why we can't have two_plus_two_eq and two_plus_two_eq_four