disjointUnion — Mathlib

Lean4
/-- Combine two `PartialEquiv`s with disjoint sources and disjoint targets. We reuse
`PartialEquiv.piecewise`, then override `source` and `target` to ensure better definitional
equalities. -/
@[simps! -fullyApplied]
def disjointUnion (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)] : PartialEquiv α β :=
  (e.piecewise e' e.source e.target e.isImage_source_target <|
        e'.isImage_source_target_of_disjoint _ hs.symm ht.symm).copy
    _ rfl _ rfl (e.source ∪ e'.source) (ite_left _ _) (e.target ∪ e'.target) (ite_left _ _)
Похожие утверждения