disjoint_sUnion_disjointOfDiffUnion

English

The union of disjointOfDiffUnion is disjoint from the union over I.

Русский

Объединение disjointOfDiffUnion попарно несовпадает с объединением I.

LaTeX

$$$$ Disjoint \\\\left( ⋃_0 (I : Set (Set α)) \\\\right) ( ⋃_0 hC.disjointOfDiffUnion hs hI ) $$$$

Lean4

theorem disjoint_sUnion_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    Disjoint (⋃₀ (I : Set (Set α))) (⋃₀ hC.disjointOfDiffUnion hs hI) := by
  rw [← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion]; exact Set.disjoint_sdiff_right

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