Mathlib Map

Theorems · Definition · algebraic topology

FundamentalGroupoid.as

{X : Type u_3} → FundamentalGroupoid X → X

View a term of FundamentalGroupoid X as a term of X.

Defined in
Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Cited by
40 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

FundamentalGroupoidFunctor.prodToProdTop · cited by 7FundamentalGroupoidFuncto…FundamentalGroupoid.map · cited by 6FundamentalGroupoid.mapFundamentalGroupoid.equiv · cited by 5FundamentalGroupoid.equivFundamentalGroupoid.ext · cited by 4FundamentalGroupoid.extFundamentalGroupoidFunctor.piToPiTop · cited by 3FundamentalGroupoidFuncto…IsQuotientCoveringMap.monodromy_eq_id_iff · cited by 3IsQuotientCoveringMap.mon…IsCoveringMap.monodromyFunctor · cited by 3IsCoveringMap.monodromyFu…ContinuousMap.Homotopy.eq_path_of_eq_image · cited by 2Homotopy.eq_path_of_eq_im…IsQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff · cited by 2IsQuotientCoveringMap.fun…IsQuotientCoveringMap.ker_monodromyPerm · cited by 2IsQuotientCoveringMap.ker…IsQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smul · cited by 2IsQuotientCoveringMap.uno…FundamentalGroup.mapOfEq_apply · cited by 2FundamentalGroup.mapOfEq_…unitInterval.uhpath01 · cited by 2unitInterval.uhpath01ContinuousMap.Homotopy.evalAt_eq · cited by 1Homotopy.evalAt_eqContinuousMap.Homotopy.heq_path_of_eq_image · cited by 1Homotopy.heq_path_of_eq_i…FundamentalGroupoid · cited by 60FundamentalGroupoidFundamentalGroupoid.asCITED BYCITES

Cites1

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

Cited by50

Results whose statement or proof uses this declaration.