Theorems · Definition · general topology

PartialEquiv.prod

{α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → PartialEquiv α β → PartialEquiv γ δ → PartialEquiv (α × γ) (β × δ)

The product of two partial equivalences, as a partial equivalence on the product.

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

29 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext