Theorems · Theorem · general topology

PartialEquiv.prod_target

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

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext