Theorems · Theorem · general topology

Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv

∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsOpenEmbedding f) [inst_2 : Nonempty X] {x : Y},
  x ∈ Set.range f → f (↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).symm x) = x

Defined in: Mathlib.Topology.OpenPartialHomeomorph.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.rangestatement and proof · cited by 4,705
OpenPartialHomeomorph.toFun'statement and proof · cited by 745
OpenPartialHomeomorph.symmstatement and proof · cited by 460
Topology.IsOpenEmbeddingstatement and proof · cited by 231
OpenPartialHomeomorph.right_invproof · cited by 38
Topology.IsOpenEmbedding.toOpenPartialHomeomorphstatement and proof · cited by 14
Topology.IsOpenEmbedding.toOpenPartialHomeomorph_applyproof · cited by 5
Topology.IsOpenEmbedding.toOpenPartialHomeomorph_targetproof · cited by 5

Cited by2

Results whose statement or proof uses this declaration.

contMDiff_isOpenEmbeddingproof · cited by 1
contMDiffOn_isOpenEmbedding_symmproof · cited by 1