Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-28 17:00 c495ed61

View on Github →

move(data/set/pairwise): Move set.pairwise_on (#9986) This moves set.pairwise_on to data.set.pairwise, where pairwise and set.pairwise_disjoint already are.

Estimated changes

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_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_singleton
deleted theorem set.pairwise_on_top
deleted theorem set.pairwise_on_union
deleted theorem set.bUnion_diff_bUnion_eq
deleted theorem set.pairwise_on_Union
deleted theorem set.pairwise_on_sUnion
modified theorem pairwise.mono
modified theorem pairwise.pairwise_on
modified def pairwise
modified theorem pairwise_disjoint_fiber
modified theorem pairwise_disjoint_on
modified theorem pairwise_disjoint_on_bool
modified theorem pairwise_on_bool
added theorem set.pairwise_on.imp
added theorem set.pairwise_on.imp_on
added theorem set.pairwise_on.mono'
added theorem set.pairwise_on.mono
added def set.pairwise_on
added theorem set.pairwise_on_Union
added theorem set.pairwise_on_empty
added theorem set.pairwise_on_insert
added theorem set.pairwise_on_pair
added theorem set.pairwise_on_sUnion
added theorem set.pairwise_on_top
added theorem set.pairwise_on_union
modified theorem set.pairwise_on_univ
modified theorem symmetric.pairwise_on