Theorems · Definition · general topology
Equiv.toPartialEquiv
{α : Type u_1} → {β : Type u_2} → α ≃ β → PartialEquiv α βAssociate a PartialEquiv to an Equiv.
- Defined in
- Mathlib.Logic.Equiv.PartialEquiv
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement and proof · cited by 8,337
- Set.univproof · cited by 3,945
- PartialEquivstatement · cited by 335
- Equiv.toPartialEquivOfImageEqproof · cited by 6
Cited by22
Results whose statement or proof uses this declaration.
- PartialEquiv.reflproof · cited by 43
- ModelWithCorners.transContinuousLinearEquivproof · cited by 14
- Equiv.transPartialEquivproof · cited by 9
- PartialEquiv.transEquivproof · cited by 9
- NumberField.mixedEmbedding.fundamentalCone.expMapBasis_posproof · cited by 7
- tangentBundle_model_space_chartAtstatement and proof · cited by 4
- Equiv.trans_toPartialEquivstatement · cited by 3
- Equiv.transPartialEquiv_eq_transstatement and proof · cited by 3
- PartialEquiv.transEquiv_eq_transstatement and proof · cited by 3
- Equiv.toPartialEquiv_sourcestatement and proof · cited by 2
- Diffeomorph.toPartialDiffeomorphproof · cited by 1
- Equiv.toPartialEquiv_applystatement and proof · cited by 1