lattice): move `Sup_sUnion` (#14077)

Commit

3 years ago

chore(order/complete_lattice,data/set/lattice): move `Sup_sUnion` (#14077) * move `Sup_sUnion` and `Inf_sUnion` to `data.set.lattice`; * golf a few proofs.

Author

urkud

Parents

bada932c

mathlib3 fa4c0368 - chore(order/complete_lattice,data/set/lattice): move `Sup_sUnion` (#14077)

mathlib3
fa4c0368 - chore(order/complete_lattice,data/set/lattice): move `Sup_sUnion` (#14077)