disjointOfDiffUnion — Mathlib

English

The empty set ∅ is not a member of hC.disjointOfDiffUnion hs hI.

Русский

Пустое множество не принадлежит hC.disjointOfDiffUnion hs hI.

LaTeX

$$$$ ∅ ∉ hC.disjointOfDiffUnion hs hI $$$$

Lean4

/-- In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`,
`disjointOfDiffUnion` is a finite set of sets in `C` such that
`s \ ⋃₀ I = ⋃₀ (hC.disjointOfDiffUnion hs I hI)`.
`disjointOfDiff` is a special case of `disjointOfDiffUnion` where `I` is a
singleton. -/
noncomputable def disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : Finset (Set α) :=
  (hC.exists_disjoint_finset_diff_eq hs hI).choose \ {∅}

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