unionSumInter — Mathlib

English

If s has decidable membership, then the sum (s ∪ t) ⊕ (s ∩ t) is naturally equivalent to s ⊕ t.

Русский

Если для множества s верно, что принадлежность детерминирована, тогда сумма (s ∪ t) ⊕ (s ∩ t) естественным образом эквивалентна s ⊕ t.

LaTeX

$$$(s \cup t) \oplus (s \cap t) \simeq s \oplus t,$ \\text{при } [\DecidablePred (\cdot \in s)].$$

Lean4

/-- If `s` is a set with decidable membership, then the sum of `s ∪ t` and `s ∩ t` is equivalent
to `s ⊕ t`. -/
protected def unionSumInter {α : Type u} (s t : Set α) [DecidablePred (· ∈ s)] :
    (s ∪ t : Set α) ⊕ (s ∩ t : Set α) ≃ s ⊕ t :=
  calc
    (s ∪ t : Set α) ⊕ (s ∩ t : Set α) ≃ (s ∪ t \ s : Set α) ⊕ (s ∩ t : Set α) := by rw [union_diff_self]
    _ ≃ (s ⊕ (t \ s : Set α)) ⊕ (s ∩ t : Set α) := (sumCongr (Set.union disjoint_sdiff_self_right) (Equiv.refl _))
    _ ≃ s ⊕ ((t \ s : Set α) ⊕ (s ∩ t : Set α)) := (sumAssoc _ _ _)
    _ ≃ s ⊕ (t \ s ∪ s ∩ t : Set α) :=
      (sumCongr (Equiv.refl _)
        (by
          refine (Set.union' (· ∉ s) ?_ ?_).symm
          exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1]))
    _ ≃ s ⊕ t := by {
      rw [(_ : t \ s ∪ s ∩ t = t)]
      rw [union_comm, inter_comm, inter_union_diff]
    }

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