refactor(data/finset): use lattice operations

[urkud]

Use ⊔, ⊓, ⊥ instead of ∪, ∩, ∅. Rename sup/inf to supr/infi to avoid
name conflicts.

---

I made data.finset compile. I'd like to know if there are any objections before porting
the rest of mathlib.

Zulip thread

[gebner]

This makes finset and set inconsistent. How about unifying the two families of operations? That is, remove Union in favor of supr and remove union in favor of sup, etc., and maybe use the notation ⋃ and ∪, etc., for both?

[urkud]

In this case what should we do with

1. Subset
2. Ssubset
3. Empty set
4. Univ?

[urkud]

This RFC was rejected.