Module docstring
{"# Translating pairwise relations on sets to lists
On a list with no duplicates, the condition of Set.Pairwise and List.Pairwise are equivalent.
"}
List.Nodup.pairwise_of_set_pairwise
theorem
{l : List α} {r : α → α → Prop} (hl : l.Nodup) (h : {x | x ∈ l}.Pairwise r) : l.Pairwise r
Full source
theorem Nodup.pairwise_of_set_pairwise {l : List α} {r : α → α → Prop} (hl : l.Nodup)
(h : {x | x ∈ l}.Pairwise r) : l.Pairwise r :=
hl.pairwise_of_forall_ne hInformal description
Let $l$ be a list of elements of type $\alpha$ with no duplicates, and let $r$ be a binary relation on $\alpha$. If the set of elements in $l$ is pairwise related by $r$, then the list $l$ itself is pairwise related by $r$.
List.Nodup.pairwise_coe
theorem
[IsSymm α r] (hl : l.Nodup) : {a | a ∈ l}.Pairwise r ↔ l.Pairwise r
Full source
@[simp]
theorem Nodup.pairwise_coe [IsSymm α r] (hl : l.Nodup) :
{ a | a ∈ l }{ a | a ∈ l }.Pairwise r ↔ l.Pairwise r := by
induction l with | nil => simp | cons a l ih => ?_
rw [List.nodup_cons] at hl
have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm
simp [Set.setOf_or, Set.pairwise_insert_of_symmetric fun _ _ ↦ symm_of r, ih hl.2, and_comm,
forall₂_congr this]Informal description
Let $\alpha$ be a type with a symmetric relation $r$, and let $l$ be a list of elements of type $\alpha$ with no duplicates. Then the set $\{a \mid a \in l\}$ is pairwise related by $r$ if and only if the list $l$ is pairwise related by $r$.