Theorems · Theorem · general topology

PartialEquiv.pi_trans

∀ {ι : Type u_5} {αi : ι → Type u_6} {βi : ι → Type u_7} {γi : ι → Type u_8} (ei : (i : ι) → PartialEquiv (αi i) (βi i))
  (ei' : (i : ι) → PartialEquiv (βi i) (γi i)),
  (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun i => (ei i).trans (ei' i)

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

0 results in Mathlib

Foundations

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