pairwiseDisjoint_disjointOfDiff — Mathlib

English

In a semiring of sets C, if s and t belong to C, then the family of sets produced by the difference operation is pairwise disjoint.

Русский

В полупарантине множеств C, если s и t принадлежат C, то семейство множеств, получаемое операцией разности, попарно непересекается.

LaTeX

$$$\\\\operatorname{PairwiseDisjoint}\\\\left(hC.disjointOfDiff hs ht : Set\\\\ (Set\\\\ α)\\\\right) \\\\ operatorname{ id }$$$

Lean4

theorem pairwiseDisjoint_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    PairwiseDisjoint (hC.disjointOfDiff hs ht : Set (Set α)) id := by
  classical
  simp only [disjointOfDiff, coe_sdiff, coe_singleton]
  exact Set.PairwiseDisjoint.subset (hC.diff_eq_sUnion' s hs t ht).choose_spec.2.1 diff_subset

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