English
Let s ⊆ t be subsets of a set A with decidable membership in s. The inverse of the sum-difference equivalence sends, in the case x ∈ t but x ∉ s, the right-hand summand to the corresponding pair representing x ∈ sᶜ ∩ t.
Русский
Пусть s ⊆ t — подмножества множества A, для которых членство в s конечно. Обратное отображение для равносвязи SumDiffSubset отправляет в случае x ∈ t и x ∉ s правый член правой части разложения на пару, соответствующий x ∈ s^c ∩ t.
LaTeX
$$$(s \cup t) \oplus (s \cap t) \;\simeq\; s \oplus t \quad\text{и}\quad \text{если } x\in t \setminus s,\; (\mathrm{sumDiffSubset}(h))^{-1}(\mathrm{Sum.inr}\langle x, x\notin s\rangle) = \mathrm{Sum.inr}\langle x, x\in t, x\notin s\rangle$$$
Lean4
theorem sumDiffSubset_symm_apply_of_notMem {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] {x : t}
(hx : x.1 ∉ s) : (Equiv.Set.sumDiffSubset h).symm x = Sum.inr ⟨x, ⟨x.2, hx⟩⟩ :=
by
apply (Equiv.Set.sumDiffSubset h).injective
simp only [apply_symm_apply, sumDiffSubset_apply_inr, Set.inclusion_mk]
