Theorems · Definition · general topology
PartialEquiv.restr
{α : Type u_1} → {β : Type u_2} → PartialEquiv α β → Set α → PartialEquiv α βRestricting a partial equivalence to e.source ∩ s
- Defined in
- Mathlib.Logic.Equiv.PartialEquiv
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- PartialEquivstatement and proof · cited by 335
- PartialEquiv.IsImage.restrproof · cited by 7
Cited by40
Results whose statement or proof uses this declaration.
- PartialEquiv.transproof · cited by 88
- ContMDiffWithinAt.compproof · cited by 18
- uniqueMDiffWithinAt_univproof · cited by 14
- Equidecomp.restrproof · cited by 9
- NumberField.mixedEmbedding.fundamentalCone.expMapBasis_posproof · cited by 7
- OpenPartialHomeomorph.restr_source_interproof · cited by 4
- PartialEquiv.restr_eq_of_source_subsetstatement · cited by 3
- Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEqproof · cited by 3
- OpenPartialHomeomorph.continuousOn_extendproof · cited by 3
- OpenPartialHomeomorph.ofSet_transproof · cited by 3
- ModelWithCorners.hasMFDerivAtproof · cited by 3