pairwise_of_coe_toFinset_pairwise

English

If a list l has its toFinset interpreted as a set pairwise disjoint under f, then l is pairwise disjoint under the function on f.

Русский

Если список l имеет свойство попарной непересекаемости через toFinset и f, то сам список l попарно непересекается относительно функции onFun Disjoint f.

LaTeX

$$hl : (l.toFinset : Set α).PairwiseDisjoint f → hn : l.Nodup → l.Pairwise f$$

Lean4

theorem pairwise_of_coe_toFinset_pairwise (hl : (l.toFinset : Set α).Pairwise r) (hn : l.Nodup) : l.Pairwise r :=
  by
  rw [coe_toFinset] at hl
  exact hn.pairwise_of_set_pairwise hl

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