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...