Commit 2024-06-11 01:22 c0f77227

View on Github →

feat(Data/Set/Basic): Lemmas about pairs (#12875) We add some basic API about two-element sets. This involves moving the 'pair' section further down the file because of the position of lemmas used in proofs.

Estimated changes

added theorem Set.pair_diff_left
added theorem Set.pair_diff_right
added theorem Set.pair_subset
added theorem Set.pair_subset_iff
added theorem Set.subset_insert_iff
added theorem Set.subset_pair_iff
added theorem Set.subset_pair_iff_eq