pairwiseDisjoint_union_disjointOfDiffUnion

English

PairwiseDisjoint (⋃ x ∈ J, hC.disjointOfUnion hJ x) id

Русский

Попарная непересекаемость по объединению дисзjointOfUnion

LaTeX

$$$$ ( (⋃ x ∈ J, (hC.disjointOfUnion hJ x : Set( Set α ))) ).PairwiseDisjoint id $$$$

Lean4

theorem pairwiseDisjoint_union_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C)
    (h_dis : PairwiseDisjoint (I : Set (Set α)) id) :
    PairwiseDisjoint (I ∪ hC.disjointOfDiffUnion hs hI : Set (Set α)) id :=
  by
  rw [pairwiseDisjoint_union]
  refine ⟨h_dis, hC.pairwiseDisjoint_disjointOfDiffUnion hs hI, fun u hu v hv _ ↦ ?_⟩
  simp_rw [id]
  exact
    disjoint_of_subset (subset_sUnion_of_mem hu) (subset_sUnion_of_mem hv)
      (hC.disjoint_sUnion_disjointOfDiffUnion hs hI)

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