Basic

📁 Source: Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Statistics

Metric	Count
Definitions FundamentalGroupoid, as, equiv, fromPath, fromTop, fundamentalGroupoidFunctor, instGroupoid, instInhabited, map, termπ, termπₓ, termπₘ, toPath, toTop, reflSymmTrans, reflTrans, reflTransSymm, reflTransSymmAux, transAssoc, transAssocReparamAux, transRefl, transReflReparamAux	22
Theorems comp_eq, conj_eqToHom, conj_eqToHom_assoc, eqToHom_eq, equiv_apply, equiv_symm_apply_as, ext, ext_iff, fromPath_eq_iff_homotopic, id_eq_path_refl, instIsEmpty, instNonempty, instSubsingleton, isEmpty_iff, map_comp, map_eq, map_id, map_map, map_obj_as, nonempty_iff, subsingleton_iff, refl_trans, symm_trans, trans_assoc, trans_refl, trans_symm, refl_trans, symm_trans, trans_assoc, trans_refl, trans_symm, continuous_reflTransSymmAux, continuous_transAssocReparamAux, continuous_transReflReparamAux, reflTransSymmAux_mem_I, transAssocReparamAux_mem_I, transAssocReparamAux_one, transAssocReparamAux_zero, transReflReparamAux_mem_I, transReflReparamAux_one, transReflReparamAux_zero, trans_assoc_reparam, trans_refl_reparam	43
Total	65

FundamentalGroupoid

Definitions

Name	Category	Theorems
as 📖	CompOp	24 math math: eqToHom_eq, equiv_symm_apply_as, ContinuousMap.Homotopy.apply_zero_path, ContinuousMap.Homotopy.evalAt_eq, map_map, ContinuousMap.Homotopy.heq_path_of_eq_image, equiv_apply, ContinuousMap.Homotopy.eq_path_of_eq_image, FundamentalGroupoidFunctor.prodToProdTop_obj, FundamentalGroupoidFunctor.piToPiTop_map, ContinuousMap.Homotopy.apply_one_path, FundamentalGroupoidFunctor.projLeft_map, comp_eq, IsCoveringMap.monodromyFunctor_obj, FundamentalGroupoidFunctor.piToPiTop_obj_as, map_obj_as, FundamentalGroupoidFunctor.projRight_map, IsCoveringMap.monodromyFunctor_map, conj_eqToHom, id_eq_path_refl, ext_iff, FundamentalGroupoidFunctor.prodToProdTop_map, FundamentalGroupoidFunctor.proj_map, ContinuousMap.Homotopy.eq_diag_path
equiv 📖	CompOp	2 math math: equiv_symm_apply_as, equiv_apply
fromPath 📖	CompOp	1 math math: fromPath_eq_iff_homotopic
fromTop 📖	CompOp	5 math math: ContinuousMap.Homotopy.apply_zero_path, ContinuousMap.Homotopy.evalAt_eq, ContinuousMap.Homotopy.eq_path_of_eq_image, ContinuousMap.Homotopy.apply_one_path, ContinuousMap.Homotopy.eq_diag_path
fundamentalGroupoidFunctor 📖	CompOp	21 math math: FundamentalGroupoidFunctor.piIso_hom, ContinuousMap.Homotopy.apply_zero_path, ContinuousMap.Homotopy.evalAt_eq, ContinuousMap.Homotopy.heq_path_of_eq_image, ContinuousMap.Homotopy.eq_path_of_eq_image, FundamentalGroupoidFunctor.prodToProdTop_obj, FundamentalGroupoidFunctor.prodIso_hom, FundamentalGroupoidFunctor.piToPiTop_map, ContinuousMap.Homotopy.apply_one_path, FundamentalGroupoidFunctor.projLeft_map, FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone, map_eq, FundamentalGroupoidFunctor.preservesProduct, FundamentalGroupoidFunctor.piToPiTop_obj_as, FundamentalGroupoidFunctor.piIso_inv, FundamentalGroupoidFunctor.prodIso_inv, FundamentalGroupoidFunctor.projRight_map, FundamentalGroupoidFunctor.prodToProdTop_map, FundamentalGroupoidFunctor.proj_map, FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone, ContinuousMap.Homotopy.eq_diag_path
instGroupoid 📖	CompOp	21 math math: eqToHom_eq, map_comp, conj_eqToHom_assoc, map_map, instSubsingletonHomPUnit, simply_connected_def, comp_eq, FundamentalGroupoidFunctor.instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso, SimplyConnectedSpace.equiv_unit, punitEquivDiscretePUnit_unitIso, IsCoveringMap.monodromyFunctor_obj, map_id, simplyConnectedSpace_iff, map_obj_as, IsCoveringMap.monodromyFunctor_map, conj_eqToHom, punitEquivDiscretePUnit_counitIso, id_eq_path_refl, punitEquivDiscretePUnit_inverse, ContinuousMap.Homotopy.hcast_def, punitEquivDiscretePUnit_functor
instInhabited 📖	CompOp	—
map 📖	CompOp	5 math math: map_comp, map_map, FundamentalGroupoidFunctor.instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso, map_id, map_obj_as
termπ 📖	CompOp	—
termπₓ 📖	CompOp	—
termπₘ 📖	CompOp	—
toPath 📖	CompOp	—
toTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp FundamentalGroupoid CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory instGroupoid Path.Homotopic.Quotient.trans as	—	—
conj_eqToHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp FundamentalGroupoid CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory instGroupoid CategoryTheory.eqToHom as Path.cast	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
conj_eqToHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp FundamentalGroupoid CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory instGroupoid CategoryTheory.eqToHom Path.cast	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' conj_eqToHom
eqToHom_eq 📖	mathematical	—	CategoryTheory.eqToHom FundamentalGroupoid CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory instGroupoid Path Path.Homotopic.setoid as Path.cast Path.refl	—	—
equiv_apply 📖	mathematical	—	DFunLike.coe Equiv FundamentalGroupoid EquivLike.toFunLike Equiv.instEquivLike equiv as	—	—
equiv_symm_apply_as 📖	mathematical	—	as DFunLike.coe Equiv FundamentalGroupoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv	—	—
ext 📖	—	as	—	—	—
ext_iff 📖	mathematical	—	as	—	ext
fromPath_eq_iff_homotopic 📖	mathematical	—	fromPath Path.Homotopic	—	—
id_eq_path_refl 📖	mathematical	—	CategoryTheory.CategoryStruct.id FundamentalGroupoid CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory instGroupoid Path as Path.Homotopic.setoid Path.refl	—	—
instIsEmpty 📖	mathematical	—	IsEmpty FundamentalGroupoid	—	Equiv.isEmpty
instNonempty 📖	mathematical	—	FundamentalGroupoid	—	Equiv.nonempty
instSubsingleton 📖	mathematical	—	FundamentalGroupoid	—	Equiv.subsingleton
isEmpty_iff 📖	mathematical	—	IsEmpty FundamentalGroupoid	—	Equiv.isEmpty_congr
map_comp 📖	mathematical	—	map ContinuousMap.comp CategoryTheory.Functor.comp FundamentalGroupoid CategoryTheory.Groupoid.toCategory instGroupoid	—	—
map_eq 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category fundamentalGroupoidFunctor TopCat.of TopCat.carrier TopCat.str CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' TopCat.ofHom Path.Homotopic.Quotient.map	—	—
map_id 📖	mathematical	—	map ContinuousMap.id CategoryTheory.Functor.id FundamentalGroupoid CategoryTheory.Groupoid.toCategory instGroupoid	—	—
map_map 📖	mathematical	—	CategoryTheory.Functor.map FundamentalGroupoid CategoryTheory.Groupoid.toCategory instGroupoid map Path.Homotopic.Quotient.map as	—	—
map_obj_as 📖	mathematical	—	as CategoryTheory.Functor.obj FundamentalGroupoid CategoryTheory.Groupoid.toCategory instGroupoid map DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	—
nonempty_iff 📖	mathematical	—	FundamentalGroupoid	—	Equiv.nonempty_congr
subsingleton_iff 📖	mathematical	—	FundamentalGroupoid	—	Equiv.subsingleton_congr

Path.Homotopic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl_trans 📖	mathematical	—	Path.Homotopic Path.trans Path.refl	—	—
symm_trans 📖	mathematical	—	Path.Homotopic Path.trans Path.symm Path.refl	—	—
trans_assoc 📖	mathematical	—	Path.Homotopic Path.trans	—	—
trans_refl 📖	mathematical	—	Path.Homotopic Path.trans Path.refl	—	—
trans_symm 📖	mathematical	—	Path.Homotopic Path.trans Path.symm Path.refl	—	—

Path.Homotopic.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl_trans 📖	mathematical	—	trans refl	—	ind Path.Homotopic.refl_trans
symm_trans 📖	mathematical	—	trans symm refl	—	ind Path.Homotopic.symm_trans
trans_assoc 📖	mathematical	—	trans	—	ind Path.Homotopic.trans_assoc
trans_refl 📖	mathematical	—	trans refl	—	ind Path.Homotopic.trans_refl
trans_symm 📖	mathematical	—	trans symm refl	—	ind Path.Homotopic.trans_symm

Path.Homotopy

Definitions

Name	Category	Theorems
reflSymmTrans 📖	CompOp	—
reflTrans 📖	CompOp	—
reflTransSymm 📖	CompOp	—
reflTransSymmAux 📖	CompOp	2 math math: reflTransSymmAux_mem_I, continuous_reflTransSymmAux
transAssoc 📖	CompOp	—
transAssocReparamAux 📖	CompOp	5 math math: continuous_transAssocReparamAux, transAssocReparamAux_mem_I, transAssocReparamAux_zero, transAssocReparamAux_one, trans_assoc_reparam
transRefl 📖	CompOp	—
transReflReparamAux 📖	CompOp	5 math math: transReflReparamAux_one, transReflReparamAux_zero, transReflReparamAux_mem_I, continuous_transReflReparamAux, trans_refl_reparam

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_reflTransSymmAux 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace reflTransSymmAux	—	continuous_if_le OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.comp' continuous_subtype_val Continuous.snd continuous_id' continuous_const ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.comp_continuousOn' ContinuousOn.fst continuousOn_id' continuousOn_const ContinuousOn.snd ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal
continuous_transAssocReparamAux 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace transAssocReparamAux	—	continuous_if_le OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_subtype_val continuous_const ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousOn_const Continuous.continuousOn ContinuousOn.fun_add IsTopologicalSemiring.toContinuousAdd
continuous_transReflReparamAux 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace transReflReparamAux	—	continuous_if_le OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_subtype_val continuous_const ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousOn_const Continuous.continuousOn
reflTransSymmAux_mem_I 📖	mathematical	—	Real Set Set.instMembership unitInterval reflTransSymmAux	—	mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing mul_assoc mul_le_one₀ IsOrderedRing.toMulPosMono
transAssocReparamAux_mem_I 📖	mathematical	—	Real Set Set.instMembership unitInterval transAssocReparamAux	—	le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le unitInterval.nonneg Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toCharZero Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg lt_of_not_ge CancelDenoms.add_subst Mathlib.Meta.NormNum.IsNat.to_raw_eq CancelDenoms.mul_subst unitInterval.le_one
transAssocReparamAux_one 📖	mathematical	—	transAssocReparamAux Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing Real.instOne	—	Real.instIsOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isRat_le_false IsStrictOrderedRing.toNontrivial Mathlib.Meta.NormNum.IsNNRat.to_isRat mul_one Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add IsUnit.div_mul_cancel Mathlib.Meta.NormNum.isNat_eq_false Nat.cast_zero
transAssocReparamAux_zero 📖	mathematical	—	transAssocReparamAux Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Real.instZero	—	Real.instIsOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Nat.cast_zero MulZeroClass.mul_zero zero_add mul_one
transReflReparamAux_mem_I 📖	mathematical	—	Real Set Set.instMembership unitInterval transReflReparamAux	—	le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le unitInterval.nonneg Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toCharZero Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.add_lt_of_le_of_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one
transReflReparamAux_one 📖	mathematical	—	transReflReparamAux Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing Real.instOne	—	Real.instIsOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isRat_le_false IsStrictOrderedRing.toNontrivial Mathlib.Meta.NormNum.IsNNRat.to_isRat mul_one
transReflReparamAux_zero 📖	mathematical	—	transReflReparamAux Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Real.instZero	—	Real.instIsOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Nat.cast_zero MulZeroClass.mul_zero
trans_assoc_reparam 📖	mathematical	—	Path.trans Path.reparam Real Set Set.instMembership unitInterval transAssocReparamAux transAssocReparamAux_mem_I Set.Elem Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing transAssocReparamAux_zero Set.Icc.instOne transAssocReparamAux_one	—	Path.ext transAssocReparamAux_mem_I Real.instIsOrderedRing transAssocReparamAux_zero transAssocReparamAux_one Nat.instAtLeastTwoHAddOfNat unitInterval.mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid unitInterval.two_mul_sub_one_mem_iff LT.lt.le not_le Path.trans_apply Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt lt_of_not_ge Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos CancelDenoms.mul_subst CancelDenoms.add_subst Mathlib.Tactic.Linarith.sub_nonpos_of_le
trans_refl_reparam 📖	mathematical	—	Path.trans Path.refl Path.reparam Real Set Set.instMembership unitInterval transReflReparamAux transReflReparamAux_mem_I Set.Elem Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing transReflReparamAux_zero Set.Icc.instOne transReflReparamAux_one	—	Path.ext transReflReparamAux_mem_I Real.instIsOrderedRing transReflReparamAux_zero transReflReparamAux_one

(root)

Definitions

Name	Category	Theorems
FundamentalGroupoid 📖	CompData	29 math math: FundamentalGroupoid.eqToHom_eq, FundamentalGroupoid.map_comp, FundamentalGroupoid.equiv_symm_apply_as, FundamentalGroupoid.conj_eqToHom_assoc, FundamentalGroupoid.instSubsingleton, FundamentalGroupoid.map_map, FundamentalGroupoid.equiv_apply, FundamentalGroupoid.nonempty_iff, FundamentalGroupoid.instSubsingletonHomPUnit, simply_connected_def, FundamentalGroupoid.comp_eq, FundamentalGroupoidFunctor.instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso, SimplyConnectedSpace.equiv_unit, FundamentalGroupoid.instIsEmpty, FundamentalGroupoid.punitEquivDiscretePUnit_unitIso, IsCoveringMap.monodromyFunctor_obj, FundamentalGroupoid.map_id, simplyConnectedSpace_iff, FundamentalGroupoid.instNonempty, FundamentalGroupoid.map_obj_as, FundamentalGroupoid.subsingleton_iff, IsCoveringMap.monodromyFunctor_map, FundamentalGroupoid.conj_eqToHom, FundamentalGroupoid.isEmpty_iff, FundamentalGroupoid.punitEquivDiscretePUnit_counitIso, FundamentalGroupoid.id_eq_path_refl, FundamentalGroupoid.punitEquivDiscretePUnit_inverse, ContinuousMap.Homotopy.hcast_def, FundamentalGroupoid.punitEquivDiscretePUnit_functor

---

← Back to Index