feat(Data/Quot): toSet and equivClassOf

[SnirBroshi]

Define toSet which gets the set corresponding to an element of a quotient, and equivClassOf which gets the equivalence class of an element under a quotient.

---

I found these definitions helpful when working with quotients, specifically ConnectedComponents of a TopologicalSpace.

[github-actions]

PR summary 738faa5527

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ equivClassOf_eq_iff_apply
+ equivClassOf_eq_iff_equiv
+ equivClassOf_eq_of_r
+ instance {α : Type*} (r : α → α → Prop) : SetLike (Quot r) α
+ instance {α : Type*} (s : Setoid α) : SetLike (Quotient s) α
++ equivClassOf
++ equivClassOf_eq_iff_mk_eq
++ lift_equivClassOf_eq_toSet
++ mem_equivClassOf_self
++ mem_toSet_mk_self
++ mk_preimage_singleton_eq_toSet
++ nonempty_equivClassOf
++ nonempty_toSet
++ range_equivClassOf_equiv
++ range_toSet_eq_range_equivClassOf
++ range_toSet_equiv
++ toSet
++ toSet_injective
++ toSet_mk_eq_equivClassOf
++ union_equivClassOf_eq_univ
++ union_toSet_eq_univ

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

My initial reaction is that either we already have this or we don't want it (or perhaps both).

Maybe @kbuzzard remembers PRing a docstring arguing against something like this in the past?

[TwoFX]

Yes, I agree with Eric here. I think it would be good to start a Zulip discussion on this, including the motivating examples. It's quite possible that there is a better approach in the topology and graph theory use cases.

[SnirBroshi]

Maybe kbuzzard remembers PRing a docstring arguing against something like this in the past?

FWIW I just found a video by Kevin where they create a similar API: https://www.youtube.com/watch?v=QI-fEXSX1BA&t=47m10s