Theorems · Definition · general topology
PartialEquiv.symm
{α : Type u_1} → {β : Type u_2} → PartialEquiv α β → PartialEquiv β αThe inverse of a partial equivalence
- Defined in
- Mathlib.Logic.Equiv.PartialEquiv
- Cited by
- 453 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 13 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialEquiv.sourceproof · cited by 964
- PartialEquiv.toFunproof · cited by 821
- PartialEquiv.targetproof · cited by 650
- PartialEquivstatement and proof · cited by 335
- PartialEquiv.invFunproof · cited by 43
- PartialEquiv.map_source'proof · cited by 9
- PartialEquiv.right_inv'proof · cited by 6
- PartialEquiv.left_inv'proof · cited by 6
- PartialEquiv.map_target'proof · cited by 4
Cited by506
Results whose statement or proof uses this declaration.
- ModelWithCorners.symmproof · cited by 146
- mfderivWithinproof · cited by 126
- PartialEquiv.transproof · cited by 88
- UniqueMDiffWithinAtproof · cited by 83
- HasMFDerivWithinAtproof · cited by 65
- writtenInExtChartAtproof · cited by 54
- VectorField.mlieBracketWithinproof · cited by 45
- PartialHomeomorph.symmproof · cited by 38
- PartialEquiv.left_invstatement · cited by 37
- PartialEquiv.prodproof · cited by 29
- MDifferentiableWithinAt.hasMFDerivWithinAtproof · cited by 26
- Bundle.Pretrivialization.symmproof · cited by 26
Showing the 200 most cited of 506.