mathlib3

fa49a635 - feat(set/lattice): nonempty_of_union_eq_top_of_nonempty (#7254)

feat(set/lattice): nonempty_of_union_eq_top_of_nonempty (#7254) I have no idea where these lemmas belong. This is the earliest possible point. But perhaps they are too specific, and only belong at the point of use? I'm not certain here. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>