Theorems · Theorem · general topology

PartialEquiv.prod_trans

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {η : Type u_5} {ε : Type u_6} (e : PartialEquiv α β)
  (f : PartialEquiv β γ) (e' : PartialEquiv δ η) (f' : PartialEquiv η ε),
  (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

4 results in Mathlib

Foundations

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