disjointOfUnion — Mathlib

English

The difference s \\ ⋃₀ I equals the disjointOfDiffUnion union's sUnion.

Русский

Разность s \\ ⋃₀ I равна объединению sUnion для disjointOfDiffUnion.

LaTeX

$$$$ s \\\\setminus ⋃_0 I = ⋃_0 hC.disjointOfDiffUnion hs hI $$$$

Lean4

/-- For some `hJ : J ⊆ C` and `j : Set α`, where `hC : IsSetSemiring C`, this is
a `Finset (Set α)` such that `K j := hC.disjointOfUnion hJ` are disjoint
and `⋃₀ K j ⊆ j`, for `j ∈ J`.
Using these we write `⋃₀ J` as a disjoint union `⋃₀ J = ⋃₀ ⋃ x ∈ J, (K x)`.
See `MeasureTheory.IsSetSemiring.disjointOfUnion_props`. -/
noncomputable def disjointOfUnion (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (j : Set α) :=
  (hC.disjointOfUnion_props hJ).choose j

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