pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint

English

If the toFinset of a list l is pairwiseDisjoint with respect to f, then l is pairwise Disjoint under onFun Disjoint f.

Русский

Если toFinset списка l попарно непересекается относительно f, то сам список l попарно непересекается относительно Disjoint f.

LaTeX

$$hl : (l.toFinset : Set ι).PairwiseDisjoint f → hn : l.Nodup → l.Pairwise (Disjoint on f)$$

Lean4

theorem pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α ι} [PartialOrder α] [OrderBot α] [DecidableEq ι]
    {l : List ι} {f : ι → α} (hl : (l.toFinset : Set ι).PairwiseDisjoint f) (hn : l.Nodup) :
    l.Pairwise (_root_.Disjoint on f) :=
  pairwise_of_coe_toFinset_pairwise hl hn

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