Theorems · Theorem · general topology

PartialHomeomorph.ext_iff

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

Defined in

Mathlib.Topology.PartialHomeomorph.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace