disjointness condition

Stream: general

[Yaël Dillies]

There are two ways to write that a collection of sets is pairwise disjoint. The one that I see in mathlib is ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → disjoint (t x) (t y) (typically, in finset.card_bUnion), but I personally prefer the softer ∀ (x y ∈ s) z, z ∈ x → z ∈ y → x = y (the first one is basically the contrapositive of this).
Any reason to prefer the one that's already in mathlib? Maybe to work in synergy with pairwise?

[Eric Wieser]

Where did t go in your second version?

[Riccardo Brasca]

There is docs#set.pairwise_disjoint already in mathlib

[Riccardo Brasca]

So I guess one should use it

[Bhavik Mehta]

Perhaps it'd be useful to generalise that to sets of type α where α is a semilattice_inf_bot so we can use docs#disjoint (the case Yaël and I are interested in at the moment is for finsets of finsets, so this generalisation together with the coercion of finsets to sets would cover that too)