English
If the sources are disjoint and the targets are disjoint, then the disjoint union of e and e' equals a certain piecewise construction using isImage targets and sources.
Русский
Если области источников и целевых значений попарно непересекаются, тогда раздельное объединение e и e' равно конструированию piecewise с использованием условий образа.
LaTeX
$$$ e.disjointUnion e' hs ht = e.piecewise e' e.source e.target \\!\\;\\ldots \\!\\; (e'.isImage_source_target_of_disjoint _ hs.symm ht.symm) $$$
Lean4
theorem disjointUnion_eq_piecewise (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
(ht : Disjoint e.target e'.target) [∀ x, Decidable (x ∈ e.source)] [∀ y, Decidable (y ∈ e.target)] :
e.disjointUnion e' hs ht =
e.piecewise e' e.source e.target e.isImage_source_target
(e'.isImage_source_target_of_disjoint _ hs.symm ht.symm) :=
copy_eq ..
