Theorems · Theorem · general topology

PartialEquiv.trans_source

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

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

5 results in Mathlib

Foundations

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