Theorems · Theorem · general topology
PartialEquiv.left_inv
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α}, x ∈ e.source → ↑e.symm (↑e x) = x- Defined in
- Mathlib.Logic.Equiv.PartialEquiv
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- PartialEquiv.sourcestatement and proof · cited by 964
- PartialEquiv.toFunstatement · cited by 821
- PartialEquiv.symmstatement · cited by 453
- PartialEquivstatement and proof · cited by 335
- PartialEquiv.left_inv'proof · cited by 6
Cited by38
Results whose statement or proof uses this declaration.
- ContMDiffWithinAt.compproof · cited by 18
- extChartAt_to_invproof · cited by 9
- PartialEquiv.leftInvOnproof · cited by 9
- extChartAt_preimage_mem_nhdsproof · cited by 4
- PartialEquiv.source_inter_preimage_inv_preimageproof · cited by 3
- OpenPartialHomeomorph.map_extend_nhdsWithin_eq_imageproof · cited by 3
- ContMDiffWithinAt.mfderivWithinproof · cited by 3
- ContMDiffWithinAt.mlieBracketWithin_vectorFieldproof · cited by 3
- OpenPartialHomeomorph.extend_left_invproof · cited by 3
- OpenPartialHomeomorph.extend_preimage_mem_nhdsproof · cited by 3
- mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAtproof · cited by 3
- mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'proof · cited by 3