Theorems · Theorem · general topology

OpenPartialHomeomorph.lift_openEmbedding.congr_simp

∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f f_1 : X → X'} (e_f : f = f_1)
  (e e_1 : OpenPartialHomeomorph X Z),
  e = e_1 → ∀ (hf : Topology.IsOpenEmbedding f), e.lift_openEmbedding hf = e_1.lift_openEmbedding ⋯

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Constructions

Cited by

2 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceNonempty