OAI/Geometry/SingularHomology/
822 declarations, 0 contain sorry, 0 declared as axioms; 81 files
Files
- ActualSingularSubdivision.lean 20 declarations
- ActualSingularSubdivisionMap.lean 10 declarations
- AffineSimplexCone.lean 16 declarations
- AffineSimplexGeometry.lean 37 declarations
- AffineSingularRealization.lean 12 declarations
- BarycentricSubdivision.lean 18 declarations
- ChainComplexTransport.lean 7 declarations
- ChainMapRangeLift.lean 7 declarations
- CircleHomologySupport.lean 3 declarations
- CoordinateHomology.lean 21 declarations
- FiniteCoverHomology.lean 14 declarations
- FiniteCoverHomologyRawBase.lean 3 declarations
- FiniteGoodCoverHomology.lean 9 declarations
- FiniteSimplicialHomology.lean 8 declarations
- HomologyConjugacy.lean 7 declarations
- HomologyConstant.lean 5 declarations
- HomologyCycle.lean 10 declarations
- HomologyEigenvalue.lean 1 declarations
- HomologyEmpty.lean 6 declarations
- HomologyEvaluation.lean 13 declarations
- HomologyHomotopyEquiv.lean 7 declarations
- HomologyNaturality.lean 3 declarations
- HomologySpectrumFactor.lean 4 declarations
- HomologySupport.lean 9 imports, no declarations
- HomologyTransfer.lean 5 declarations
- HomologyZero.lean 13 declarations
- IteratedSubdivision.lean 14 declarations
- IteratedSubdivisionMesh.lean 8 declarations
- MapHomology.lean 14 declarations
- MapRealizedHomology.lean 6 declarations
- RecursiveSubdivisionMesh.lean 5 declarations
- SimplexCoordinates.lean 16 declarations
- SimplexSingularCompatibility.lean 1 declarations
- SimplexSingularRealization.lean 9 declarations
- SimplexSubdivisionMesh.lean 12 declarations
- SimplexSubtypeMesh.lean 4 declarations
- SimplicialMayerVietoris.lean 8 declarations
- SimplicialSphereHomology.lean 16 declarations
- SingularAcyclicModels.lean 17 declarations
- SingularAugmentation.lean 13 declarations
- SingularChainFoundations.lean 8 imports, no declarations
- SingularChainInclusion.lean 4 declarations
- SingularChainsFinsupp.lean 15 declarations
- SingularChainsFinsuppBoundary.lean 17 declarations
- SingularCoverChains.lean 12 declarations
- SingularCoverNaturality.lean 9 declarations
- SingularCoverNaturalityExtended.lean 9 declarations
- SingularCycleFilling.lean 11 declarations
- SingularMayerVietorisSupport.lean 5 imports, no declarations
- SingularRealizedSmallness.lean 4 declarations
- SingularSimplexCircleLift.lean 15 declarations
- SingularSimplexLebesgue.lean 6 declarations
- SingularSmallChainSupport.lean 14 declarations
- SingularSmallChains.lean 19 declarations
- SingularSmallComparison.lean 3 declarations
- SingularSmallNaturality.lean 23 declarations
- SingularSubdivision.lean 30 declarations
- SingularSubdivisionEventuallySmall.lean 3 declarations
- SingularSubdivisionIterateRealization.lean 5 declarations
- SingularSubdivisionSmallness.lean 4 declarations
- SingularSubdivisionSupport.lean 18 declarations
- SingularSupportNaturality.lean 8 declarations
- SingularSupportedFilling.lean 2 declarations
- SingularUniversalChainMap.lean 12 declarations
- SingularUniversalFinsupp.lean 4 declarations
- SingularUniversalOperator.lean 17 declarations
- SkewProductHomology.lean 10 declarations
- SmallCoverMayerVietoris.lean 12 declarations
- SphereMayerVietorisEigen.lean 10 declarations
- SphereSquareHomologyTransport.lean 8 declarations
- SubdivisionQuasiIso.lean 10 declarations
- SubdivisionSubtypeMesh.lean 7 declarations
- SubdivisionSupport.lean 5 imports, no declarations
- SubdivisionSupportMesh.lean 8 declarations
- TetrahedronChainInjection.lean 13 declarations
- TetrahedronGoodCover.lean 22 declarations
- TetrahedronGoodCoverBundle.lean 3 declarations
- TetrahedronHomologyEquiv.lean 9 declarations
- TetrahedronHomologyRank.lean 19 declarations
- TetrahedronRadialHomeomorph.lean 4 declarations
- TetrahedronSingular.lean 21 declarations