English
For a nodup list l and IsSymm relation r, the set-based pairwise relation on {a | a ∈ l} is equivalent to the list-based pairwise relation on l.
Русский
При списке без повторов и симметричности отношения r взаимно совместно по множеству элементов списка эквивалентно попарности самого списка.
LaTeX
$$$[IsSymm\\;\\alpha\\;r]\\ l.Nodup \\Rightarrow (\\{a\\mid a\\in l\\}.Pairwise r \\iff l.Pairwise r)$$$
Lean4
@[simp]
theorem pairwise_coe [IsSymm α r] (hl : l.Nodup) : {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]
