English
Let s ⊆ t be subsets of a set A. The canonical bijection φ from (s ∪ t) ⊕ (s ∩ t) to s ⊕ t sends elements arising from s and t in a natural way. In particular, if x ∈ t and x ∈ s, then the inverse φ^{-1} maps the left component coming from s to the corresponding left element; equivalently, the inverse sends an element coming from s to the left summand with the same underlying x. (Dual statements hold when x ∈ t but x ∉ s.)
Русский
Пусть s ⊆ t — подмножества множества A. Обобщённое тождество φ между суммами (s ∪ t) ⊕ (s ∩ t) и s ⊕ t трактует элементы, принадлежащие либо s, либо t, в зависимости от принадлежности. В частности, если x ∈ t и x ∈ s, то обратное отображение φ^{-1} отправляет элемент из левой части, соответствующий s, в соответствующую левую часть; аналогично верно и для случая x ∈ t, x ∉ s.
LaTeX
$$$(s \cup t) \oplus (s \cap t) \;\simeq\; s \oplus t\quad\text{(дефектная биекция при } s\subseteq t\text{, декидируемость membership в }s\text{)}$$
Lean4
theorem sumDiffSubset_symm_apply_of_mem {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] {x : t} (hx : x.1 ∈ s) :
(Equiv.Set.sumDiffSubset h).symm x = Sum.inl ⟨x, hx⟩ :=
by
apply (Equiv.Set.sumDiffSubset h).injective
simp only [apply_symm_apply, sumDiffSubset_apply_inl, Set.inclusion_mk]
