pairwiseDisjoint_coe — Mathlib

English

For a family of finsets f indexed by ι, the family is pairwise disjoint as sets if and only if it is pairwise disjoint as finsets, respecting the indexation.

Русский

Для семейства конечных множеств f индекса ι верна эквивалентность: пары множеств непересекаются как множества тогда и как элементы семейства.

LaTeX

$$$s.\\;PairwiseDisjoint (f) \\iff s.\\;PairwiseDisjoint f$$$

Lean4

@[simp, norm_cast]
theorem pairwiseDisjoint_coe {ι : Type*} {s : Set ι} {f : ι → Finset α} :
    s.PairwiseDisjoint (fun i => f i : ι → Set α) ↔ s.PairwiseDisjoint f :=
  forall₅_congr fun _ _ _ _ _ => disjoint_coe

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