Exists unique in list

Stream: Is there code for X?

[Yakov Pechersky]

Do we have a simple statement to state that a term that is in a list occurs only once in the list?

[Adam Topaz]

We must have something because of how finset is defined

[Yakov Pechersky]

nodup l says that every single element exists only once. I mean that condition, but only on a single element.

[Adam Topaz]

Ah list.nodup uses pairwise...

[Adam Topaz]

You can always filter the list with the prop =x and say something about the length of the result

[Yakov Pechersky]

Basically, there is a stronger statement than this:

lemma support_le_prod_of_me {l : list (perm α)} (h : f ∈ l) (hl : l.pairwise disjoint) :
  f.support ≤ l.prod.support :=
begin
  induction l with hd l IH,
  { simpa using h },
  { rw [list.prod_cons, (disjoint_prod_right _ _).support_mul],
    { rcases h with rfl|h,
      { exact subset_union_left _ _ },
      { exact subset.trans (IH h (list.pairwise_of_pairwise_cons hl)) (subset_union_right _ _) } },
    { intros g hg,
      exact list.rel_of_pairwise_cons hl hg } }
end

[Yakov Pechersky]

Where you don't have to have l.pairwise disjoint, just disjoint f g for all g \in l, as long as f \ne g and f is in the list only once.