Theorems · Theorem · general topology
PartialEquiv.right_inv
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β}, x ∈ e.target → ↑e (↑e.symm x) = x- Defined in
- Mathlib.Logic.Equiv.PartialEquiv
- Cited by
- 24 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.toFunstatement · cited by 821
- PartialEquiv.targetstatement and proof · cited by 650
- PartialEquiv.symmstatement · cited by 453
- PartialEquivstatement and proof · cited by 335
- PartialEquiv.right_inv'proof · cited by 6
Cited by24
Results whose statement or proof uses this declaration.
- contMDiffWithinAt_sndproof · cited by 5
- contMDiffWithinAt_fstproof · cited by 4
- Bundle.Pretrivialization.proj_symm_applyproof · cited by 4
- PartialEquiv.rightInvOnproof · cited by 3
- contMDiffAt_extChartAtproof · cited by 3
- extChartAt_target_mem_nhdsWithin_of_memproof · cited by 3
- mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAtproof · cited by 3
- hasMFDerivAt_fstproof · cited by 3
- hasMFDerivAt_sndproof · cited by 3
- mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symmproof · cited by 3
- Bundle.Pretrivialization.apply_symm_applyproof · cited by 2
- PartialEquiv.symm_apply_eqproof · cited by 2