sUnion_disjointOfDiff — Mathlib

English

In a semiring of sets, the union of the disjointOfDiff pieces equals the set difference s \\ t.

Русский

В полупрямом кольце множеств объединение элементов disjointOfDiff даёт разность s \\ t.

LaTeX

$$$$\\\\bigcup_{F \\in hC.disjointOfDiff hs ht} F = s \\\\setminus t$$$$

Lean4

theorem sUnion_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : ⋃₀ hC.disjointOfDiff hs ht = s \ t :=
  by
  classical
  rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]
  simp only [disjointOfDiff, coe_sdiff, coe_singleton]
  rw [sUnion_diff_singleton_empty]

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