pairwiseDisjoint_insert_disjointOfDiff

English

The combined family obtained by inserting t into the disjointOfDiff union remains pairwise disjoint.

Русский

Объединение с добавлением t сохраняет попарную непересекаемость.

LaTeX

$$$$ \\operatorname{PairwiseDisjoint}(\\text{insert } t (hC.disjointOfDiff hs ht) : Set (Set α)) id $$$$

Lean4

theorem pairwiseDisjoint_insert_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    PairwiseDisjoint (insert t (hC.disjointOfDiff hs ht) : Set (Set α)) id :=
  by
  have h := hC.pairwiseDisjoint_disjointOfDiff hs ht
  refine PairwiseDisjoint.insert_of_notMem h (hC.notMem_disjointOfDiff hs ht) fun u hu ↦ ?_
  simp_rw [id]
  refine Disjoint.mono_right ?_ (hC.disjoint_sUnion_disjointOfDiff hs ht)
  simp only [Set.le_eq_subset]
  exact subset_sUnion_of_mem hu

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