Theorems · Inductive type · order theory
PEquiv
Type u → Type v → Type (max u v)
A PEquiv is a partial equivalence, a representation of a bijection between a subset
of α and a subset of β. See also PartialEquiv for a version that requires toFun and
invFun to be globally defined functions and has source and target sets as extra fields.
- Defined in
- Mathlib.Data.PEquiv
- Cited by
- 75 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by90
Results whose statement or proof uses this declaration.
- PEquiv.toMatrixstatement and proof · cited by 25
- PEquiv.symmstatement and proof · cited by 23
- Equiv.toPEquivstatement · cited by 23
- PEquiv.transstatement and proof · cited by 20
- PEquiv.singlestatement · cited by 16
- PEquiv.extstatement and proof · cited by 10
- PEquiv.ofSetstatement · cited by 10
- PEquiv.reflstatement · cited by 10
- PEquiv.eq_some_iffstatement and proof · cited by 7
- PEquiv.mem_iff_memstatement and proof · cited by 3
- PEquiv.symm_injectivestatement · cited by 3
- PEquiv.toMatrix_transstatement and proof · cited by 3