leanprover-community
TODO: unify `disjoint`
Introduce disjoint on has_mem and unify the list, multiset, finset instances. The finset instance would be generalized by removing the requirement for decidable_eq
Just curious what your idea is. This would be a different definition from the root disjoint in data/set/lattice.lean?
def disjoint (a b : α) : Prop := a ⊓ b = ⊥
Would you define something like this?
def disjoint [has_mem α γ] (s t : γ) : Prop := ∀ ⦃a : α⦄, a ∈ s → a ∈ t → false
How does this affect the finset disjoint?
I changed the definition of disjoint in my local copy to s \cap t <= \bot, which works much better with existing definitions in list and multiset and set. I'll push it soonish and then we can fiddle some more if it's still not working well.
It would generalize disjoint on finset, as it would require anymore decidable_eq
@digama0 pushed the change mentioned above in https://github.com/leanprover-community/mathlib/commit/bdc90f6cef3040751df213455c02a0b520b56c50#diff-fcfc782476bb085e78399cffbe5ef17d89cac39446fa8e27de27224019d0f7acR532
Perhaps we should leave this open as a "document why we use ≤ in the definition" issue