pairwiseDisjoint_biUnion_disjointOfUnion

English

The union over J of disjointOfUnion hJ x is pairwise disjoint.

Русский

Объединение по J элементов disjointOfUnion образует попарно непересекающееся множество.

LaTeX

$$$$ (\\\\bigcup x ∈ J, (hC.disjointOfUnion hJ x : Set (Set α))) \\\\operatorname{PairwiseDisjoint} id $$$$

Lean4

theorem pairwiseDisjoint_biUnion_disjointOfUnion (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) :
    PairwiseDisjoint (⋃ x ∈ J, (hC.disjointOfUnion hJ x : Set (Set α))) id :=
  (Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.2.1

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