Theorems · Theorem · general topology

PartialEquiv.prod_symm

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ),
  (e.prod e').symm = e.symm.prod e'.symm

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

7 results in Mathlib

Foundations

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