Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 17:35 0c0ee7b0

View on Github →

refactor(data/set/pairwise): Make arguments of set.pairwise semi-implicit (#10740) The previous definition was ∀ x ∈ s, ∀ y ∈ s, x ≠ y → r x y. It now is ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y. The explicitness resulted in a lot of useless _ and general pain using set.pairwise, set.pairwise_disjoint, zorn.chain, is_antichain...

Estimated changes