Theorems · Definition · general topology

PartialEquiv.piecewise

{α : Type u_1} →
  {β : Type u_2} →
    (e e' : PartialEquiv α β) →
      (s : Set α) →
        (t : Set β) →
          [(x : α) → Decidable (x ∈ s)] →
            [(y : β) → Decidable (y ∈ t)] → e.IsImage s t → e'.IsImage s t → PartialEquiv α β

Combine two PartialEquivs using Set.piecewise. The source of the new PartialEquiv is s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s, and similarly for target. The function sends e.source ∩ s to e.target ∩ t using e and e'.source \ s to e'.target \ t using e', and similarly for the inverse function. The definition assumes e.isImage s t and e'.isImage s t.

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

8 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

DecidableDecidable