Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-21 19:52 9b60e0f7

View on Github →

feat(data/set/basic): add pairwise_on_pair (#8789) Add set.pairwise_on_insert, set.pairwise_on_pair, and set.pairwise_on_pair_of_symmetric.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.pairwise_on_insert

added theorem set.pairwise_on_pair

added theorem set.pairwise_on_pair_of_symmetric