Commit 2023-10-01 12:14 aef04106

View on Github →

chore: Make Set/Finset lemmas match lattice lemma names (#7378) Rename union_eq_left_iff_subset to union_eq_left to match sup_eq_left. Similarly for the right and inter versions.

Estimated changes

added theorem Finset.inter_eq_left
added theorem Finset.inter_eq_right
added theorem Finset.left_eq_union
added theorem Finset.right_eq_union
added theorem Finset.union_eq_empty
deleted theorem Finset.union_eq_empty_iff
added theorem Finset.union_eq_left
added theorem Finset.union_eq_right
added theorem Set.inter_eq_left
added theorem Set.inter_eq_right
added theorem Set.union_eq_left
added theorem Set.union_eq_right