Mathlib Map

Theorems · Theorem · general topology

PartialEquiv.refl_trans

∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), (PartialEquiv.refl α).trans e = e
Defined in
Mathlib.Logic.Equiv.PartialEquiv
Cited by
15 results in Mathlib
Foundations
Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ModelWithCorners.contMDiff · cited by 4ModelWithCorners.contMDiffModelWithCorners.contMDiffOn_symm · cited by 3ModelWithCorners.contMDif…FiberBundle.extChartAt · cited by 3FiberBundle.extChartAtModelWithCorners.isImmersionAtOfComplement · cited by 2ModelWithCorners.isImmers…mfderiv_chartAt_eq_tangentCoordChange · cited by 2mfderiv_chartAt_eq_tangen…mdifferentiableOn_iff_target · cited by 1mdifferentiableOn_iff_tar…contMDiffOn_iff_target · cited by 1contMDiffOn_iff_targetcontMDiffOn_isOpenEmbedding_symm · cited by 1contMDiffOn_isOpenEmbeddi…trivializationAt_model_space_apply · cited by 1trivializationAt_model_sp…contMDiff_tangentBundleModelSpaceHomeomorph · cited by 1contMDiff_tangentBundleMo…contMDiff_isOpenEmbedding · cited by 1contMDiff_isOpenEmbeddingwrittenInExtChartAt_chartAt · cited by 0writtenInExtChartAt_chart…writtenInExtChartAt_chartAt_symm · cited by 0writtenInExtChartAt_chart…OpenPartialHomeomorph.refl_trans · cited by 0OpenPartialHomeomorph.ref…contMDiff_tangentBundleModelSpaceHomeomorph_symm · cited by 0contMDiff_tangentBundleMo…PartialEquiv.source · cited by 964PartialEquiv.sourcePartialEquiv · cited by 335PartialEquivSet.univ_inter · cited by 258Set.univ_interPartialEquiv.trans · cited by 88PartialEquiv.transPartialEquiv.refl · cited by 43PartialEquiv.reflPartialEquiv.ext · cited by 19PartialEquiv.extPartialEquiv.refl_transCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by15

Results whose statement or proof uses this declaration.