pairwiseDisjoint_disjointOfDiffUnion

English

The family hC.disjointOfDiffUnion hs hI is pairwise disjoint.

Русский

Семейство hC.disjointOfDiffUnion hs hI попарно непересекается.

LaTeX

$$$$ (hC.disjointOfDiffUnion hs hI).toSet.PairwiseDisjoint id $$$$

Lean4

theorem pairwiseDisjoint_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    PairwiseDisjoint (hC.disjointOfDiffUnion hs hI : Set (Set α)) id := by
  classical
  simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton]
  exact Set.PairwiseDisjoint.subset (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.1 diff_subset

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