pairwiseDisjoint_disjointOfUnion_of_mem

English

Let C be a semiring of subsets of α. Let J be a finite collection of sets with J ⊆ C, and let j be an element of J. Then the family of blocks produced by the disjoint-union construction hC.disjointOfUnion hJ j is pairwise disjoint.

Русский

Пусть C — полукольцо подмножеств α. Пусть J — конечное подмножество; J ⊆ C, и выбрано j ∈ J. Тогда множество блоков, получаемых операцией disjointOfUnion, образуется попарно непересекающимся.

LaTeX

$$$\text{PairwiseDisjoint}\bigl(h_C\.disjointOfUnion(h_J, j) : \mathrm{Set}(\mathrm{Set}(\alpha))\bigr).$$$

Lean4

theorem pairwiseDisjoint_disjointOfUnion_of_mem (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
    PairwiseDisjoint (hC.disjointOfUnion hJ j : Set (Set α)) id :=
  by
  apply PairwiseDisjoint.subset (hC.pairwiseDisjoint_biUnion_disjointOfUnion hJ)
  exact subset_iUnion₂_of_subset j hj fun ⦃a⦄ a ↦ a

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