Theorems · Definition · general topology

PartialEquiv.pi

{ι : Type u_5} →
  {αi : ι → Type u_6} →
    {βi : ι → Type u_7} → ((i : ι) → PartialEquiv (αi i) (βi i)) → PartialEquiv ((i : ι) → αi i) ((i : ι) → βi i)

The product of a family of partial equivalences, as a partial equivalence on the pi type.

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

8 results in Mathlib

Foundations

Depth 8 from the axioms · uses Quot.sound