Theorems · Theorem · general topology

PartialEquiv.piecewise_apply

∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [inst : (x : α) → Decidable (x ∈ s)]
  [inst_1 : (y : β) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t),
  ↑(e.piecewise e' s t H H') = s.piecewise ↑e ↑e'

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableDecidable