Zulip Chat Archive

Stream: general

Topic: disjointness condition


Yaël Dillies (Jun 19 2021 at 10:58):

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 (Jun 19 2021 at 11:20):

Where did t go in your second version?

Riccardo Brasca (Jun 19 2021 at 11:23):

There is docs#set.pairwise_disjoint already in mathlib

Riccardo Brasca (Jun 19 2021 at 11:24):

So I guess one should use it

Bhavik Mehta (Jun 19 2021 at 18:48):

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)


Last updated: Dec 20 2023 at 11:08 UTC