Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 00:02 951c063d

View on Github →

chore(data/set/pairwise): rename set.pairwise_on to set.pairwise to match list.pairwise and multiset.pairwise (#10035)

Estimated changes

modified theorem finprod_mem_sUnion
deleted theorem pairwise.pairwise_on
added theorem pairwise.set_pairwise
added theorem set.pairwise.imp
added theorem set.pairwise.imp_on
added theorem set.pairwise.mono'
added theorem set.pairwise.mono
added theorem set.pairwise_Union
added theorem set.pairwise_empty
added theorem set.pairwise_insert
added theorem set.pairwise_of_forall
deleted theorem set.pairwise_on.imp
deleted theorem set.pairwise_on.imp_on
deleted theorem set.pairwise_on.mono'
deleted theorem set.pairwise_on.mono
deleted def set.pairwise_on
deleted theorem set.pairwise_on_Union
deleted theorem set.pairwise_on_empty
deleted theorem set.pairwise_on_insert
deleted theorem set.pairwise_on_of_forall
deleted theorem set.pairwise_on_pair
deleted theorem set.pairwise_on_sUnion
deleted theorem set.pairwise_on_singleton
deleted theorem set.pairwise_on_top
deleted theorem set.pairwise_on_union
deleted theorem set.pairwise_on_univ
added theorem set.pairwise_pair
added theorem set.pairwise_sUnion
added theorem set.pairwise_singleton
added theorem set.pairwise_top
added theorem set.pairwise_union
added theorem set.pairwise_univ
modified def zorn.chain