pairwise_iff_coe_toFinset_pairwise

English

For a nodup list l and a symmetric relation r, (l.toFinset : Set α).Pairwise r is equivalent to List.Pairwise r l.

Русский

Для списка без повторов l и симметричного отношения r эквивалентны: (l.toFinset).Pairwise r и List.Pairwise r l.

LaTeX

$$(hn : l.Nodup) (hs : Symmetric r) : (l.toFinset : Set α).Pairwise r ↔ l.Pairwise r$$

Lean4

theorem pairwise_iff_coe_toFinset_pairwise (hn : l.Nodup) (hs : Symmetric r) :
    (l.toFinset : Set α).Pairwise r ↔ l.Pairwise r :=
  by
  letI : IsSymm α r := ⟨hs⟩
  rw [coe_toFinset, hn.pairwise_coe]

Похожие утверждения