Theorems · Theorem · general topology

PartialEquiv.image_trans_source

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  ↑e '' (e.trans e').source = e.target ∩ e'.source

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

2 results in Mathlib

Foundations

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