Documentation Verification Report

InducedMaps

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

Statistics

Metric	Count
Definitions `diagonalPath`, `diagonalPath'`, `hcast`, `prodToProdTopI`, `uliftMap`, `equivOfHomotopyEquiv`, `homotopicMapsNatIso`, `path01`, `uhpath01`, `upath01`	10
Theorems `apply_one_path`, `apply_zero_path`, `eq_diag_path`, `eq_path_of_eq_image`, `evalAt_eq`, `hcast_def`, `heq_path_of_eq_image`, `ulift_apply`, `instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso`, `map_trans_evalAt`	10
Total	20

ContinuousMap.Homotopy

Definitions

Name	Category	Theorems
`diagonalPath` 📖	CompOp	—
`diagonalPath'` 📖	CompOp	1 math math: `eq_diag_path`
`hcast` 📖	CompOp	5 math math: `apply_zero_path`, `evalAt_eq`, `eq_path_of_eq_image`, `apply_one_path`, `hcast_def`
`prodToProdTopI` 📖	CompOp	3 math math: `apply_zero_path`, `evalAt_eq`, `apply_one_path`
`uliftMap` 📖	CompOp	4 math math: `apply_zero_path`, `evalAt_eq`, `ulift_apply`, `apply_one_path`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_one_path` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `CategoryTheory.Grpd` `CategoryTheory.Grpd.category` `FundamentalGroupoid.fundamentalGroupoidFunctor` `TopCat.of` `TopCat.carrier` `TopCat.str` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.Grpd.str'` `TopCat.ofHom` `FundamentalGroupoid.fromTop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `ContinuousMap.Homotopy` `Set.Elem` `Real` `unitInterval` `instFunLike` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `hcast` `apply_one` `instTopologicalSpaceProd` `ULift.topologicalSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `uliftMap` `CategoryTheory.prod'` `FundamentalGroupoidFunctor.prodToProdTop` `prodToProdTopI` `CategoryTheory.CategoryStruct.id` `TopCat.Hom.hom` `FundamentalGroupoid.as`	—	`Real.instIsOrderedRing` `apply_one` `eq_path_of_eq_image` `Path.prod_coe` `ulift_apply`
`apply_zero_path` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `CategoryTheory.Grpd` `CategoryTheory.Grpd.category` `FundamentalGroupoid.fundamentalGroupoidFunctor` `TopCat.of` `TopCat.carrier` `TopCat.str` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.Grpd.str'` `TopCat.ofHom` `FundamentalGroupoid.fromTop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `ContinuousMap.Homotopy` `Set.Elem` `Real` `unitInterval` `instFunLike` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `hcast` `apply_zero` `instTopologicalSpaceProd` `ULift.topologicalSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `uliftMap` `CategoryTheory.prod'` `FundamentalGroupoidFunctor.prodToProdTop` `prodToProdTopI` `CategoryTheory.CategoryStruct.id` `TopCat.Hom.hom` `FundamentalGroupoid.as`	—	`Real.instIsOrderedRing` `apply_zero` `eq_path_of_eq_image` `Path.prod_coe` `ulift_apply`
`eq_diag_path` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `CategoryTheory.Grpd` `CategoryTheory.Grpd.category` `FundamentalGroupoid.fundamentalGroupoidFunctor` `TopCat.of` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.Grpd.str'` `CategoryTheory.Functor.map` `TopCat.ofHom` `FundamentalGroupoid.fromTop` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `Path` `FundamentalGroupoid.as` `Path.Homotopic.setoid` `evalAt` `diagonalPath'`	—	`Real.instIsOrderedRing` `apply_zero` `apply_zero_path` `apply_one` `apply_one_path` `evalAt_eq` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans` `CategoryTheory.eqToHom_refl` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`eq_path_of_eq_image` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `TopCat.carrier` `TopCat.str` `ContinuousMap.instFunLike` `Path` `Set.Elem` `Real` `unitInterval` `Path.instFunLike`	`CategoryTheory.Functor.map` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `CategoryTheory.Grpd` `CategoryTheory.Grpd.category` `FundamentalGroupoid.fundamentalGroupoidFunctor` `TopCat.of` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.Grpd.str'` `TopCat.ofHom` `FundamentalGroupoid.as` `Path.Homotopic.setoid` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `FundamentalGroupoid.fromTop` `hcast` `TopCat.Hom.hom`	—	`FundamentalGroupoid.ext` `CategoryTheory.conj_eqToHom_iff_heq` `heq_path_of_eq_image`
`evalAt_eq` 📖	mathematical	—	`Path` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `Path.Homotopic.setoid` `FundamentalGroupoid.as` `FundamentalGroupoid.fromTop` `TopCat.of` `evalAt` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `CategoryTheory.Grpd` `CategoryTheory.Grpd.category` `FundamentalGroupoid.fundamentalGroupoidFunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.Grpd.str'` `ContinuousMap.Homotopy` `Set.Elem` `Real` `unitInterval` `instFunLike` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `hcast` `apply_zero` `instTopologicalSpaceProd` `ULift.topologicalSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CategoryTheory.Functor.map` `TopCat.ofHom` `uliftMap` `CategoryTheory.prod'` `FundamentalGroupoidFunctor.prodToProdTop` `Set.Icc.instOne` `prodToProdTopI` `unitInterval.uhpath01` `CategoryTheory.CategoryStruct.id` `TopCat.Hom.hom` `apply_one`	—	`Real.instIsOrderedRing` `apply_zero` `apply_one` `FundamentalGroupoid.ext` `CategoryTheory.conj_eqToHom_iff_heq` `Path.Homotopic.hpath_hext` `ContinuousMap.continuous`
`hcast_def` 📖	mathematical	—	`hcast` `CategoryTheory.eqToHom` `FundamentalGroupoid` `TopCat.carrier` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory` `FundamentalGroupoid.instGroupoid` `TopCat.str` `FundamentalGroupoid.ext`	—	—
`heq_path_of_eq_image` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `TopCat.carrier` `TopCat.str` `ContinuousMap.instFunLike` `Path` `Set.Elem` `Real` `unitInterval` `Path.instFunLike`	`Quiver.Hom` `CategoryTheory.Bundled.α` `CategoryTheory.Groupoid` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `CategoryTheory.Grpd` `CategoryTheory.Grpd.category` `FundamentalGroupoid.fundamentalGroupoidFunctor` `TopCat.of` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Groupoid.toCategory` `CategoryTheory.Grpd.str'` `CategoryTheory.Functor.map` `TopCat.ofHom` `FundamentalGroupoid.as` `Path.Homotopic.setoid`	—	`Path.Homotopic.hpath_hext` `ContinuousMap.continuous`
`ulift_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `TopCat.carrier` `TopCat.of` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceProd` `ULift.topologicalSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `TopCat.str` `ContinuousMap.instFunLike` `uliftMap` `ContinuousMap.Homotopy` `instFunLike`	—	—

FundamentalGroupoidFunctor

Definitions

Name	Category	Theorems
`equivOfHomotopyEquiv` 📖	CompOp	—
`homotopicMapsNatIso` 📖	CompOp	1 math math: `instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `FundamentalGroupoid` `CategoryTheory.Groupoid.toCategory` `FundamentalGroupoid.instGroupoid` `CategoryTheory.Functor.category` `FundamentalGroupoid.map` `homotopicMapsNatIso`	—	`CategoryTheory.NatIso.isIso_of_isIso_app` `CategoryTheory.IsGroupoid.all_isIso` `CategoryTheory.instIsGroupoid`

Path.Homotopic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_trans_evalAt` 📖	mathematical	—	`Path.Homotopic` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `Path.trans` `Path.map` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `ContinuousMap.Homotopy.evalAt`	—	`Path.continuousMapClass` `Real.instIsOrderedRing` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `ContinuousMap.continuous` `Path.source` `ContinuousMap.Homotopy.apply_zero` `Path.target` `ContinuousMap.Homotopy.apply_one` `Path.ext` `Nat.instAtLeastTwoHAddOfNat` `unitInterval.two_mul_sub_one_mem_iff` `LT.lt.le` `not_le` `one_div` `unitInterval.mul_pos_mem_iff` `zero_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Path.map_coe` `Path.trans_apply`

unitInterval

Definitions

Name	Category	Theorems
`path01` 📖	CompOp	—
`uhpath01` 📖	CompOp	1 math math: `ContinuousMap.Homotopy.evalAt_eq`
`upath01` 📖	CompOp	—

---

← Back to Index