Theorems · Theorem · general topology

PartialHomeomorph.ext

∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : PartialHomeomorph X Y),
  (∀ (x : X), ↑e x = ↑e' x) → (∀ (x : Y), ↑e.symm x = ↑e'.symm x) → e.source = e'.source → e = e'

Two partial homeomorphisms are equal when they have equal toFun, invFun and source. It is not sufficient to have equal toFun and source, as this only determines invFun on the target. This would only be true for a weaker notion of equality, arguably the right one, called EqOnSource.

Defined in

Mathlib.Topology.PartialHomeomorph.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace