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