`OAI/Geometry/HyperbolicGroups/`

4538 declarations, 0 contain sorry, 0 declared as axioms; 422 files

Files

ActualContact.lean 13 declarations
ActualDegree.lean 4 declarations
ActualFaceCounts.lean 15 declarations
ActualFragment.lean 7 declarations
ActualLabel.lean 4 declarations
ActualLayers.lean 6 declarations
ActualLiftedChain.lean 3 declarations
ActualOccurrenceShape.lean 19 declarations
ActualPartition.lean 7 declarations
ActualPosition.lean 6 declarations
ActualRawAccount.lean 2 declarations
ActualRawCount.lean 10 declarations
ActualWeights.lean 4 declarations
AnnularSeparator.lean 2 declarations
BFSLevels.lean 3 declarations
BFSTree.lean 2 declarations
BalancedGrouping.lean 1 declarations
BasedSquareContraction.lean 14 declarations
BasedTriangleContraction.lean 11 declarations
Basic.lean 23 declarations
BigonRemove.lean 12 declarations
BipartiteLink.lean 1 declarations
BoundaryEnumeration.lean 2 declarations
BoundaryEraseList.lean 6 declarations
BoundaryFold.lean 10 declarations
BoundaryGraphWalk.lean 2 declarations
BoundaryIndex.lean 6 declarations
BoundaryLift.lean 2 declarations
BoundaryList.lean 11 declarations
BoundaryRotation.lean 6 declarations
BoundarySplice.lean 2 declarations
Budget.lean 5 declarations
CATZero.lean 64 declarations
CATZeroFurther.lean 15 declarations
Candidate.lean 3 declarations
CellularFilling.lean 2 declarations
Chernoff.lean 6 declarations
ClosedCoverGluing.lean 5 declarations
ClosedPicture.lean 5 declarations
Coincidence.lean 14 declarations
ColoredApex.lean 9 declarations
CompactLocalCATGeometric.lean 3 declarations
Concentration.lean 6 declarations
ConditionalStar.lean 28 declarations
Conditioning.lean 6 declarations
ConeApexProducer.lean 6 declarations
ConeCellCollapse.lean 6 declarations
ConeCellTarget.lean 20 declarations
ConeCellWalk.lean 9 declarations
ConeCover.lean 6 declarations
ConeData.lean 25 declarations
ConeDecorationGroup.lean 3 declarations
ConeDiskNormal.lean 2 declarations
ConeExteriorWalk.lean 13 declarations
ConeFanCorner.lean 16 declarations
ConeFanGroup.lean 7 declarations
ConeFrozenTarget.lean 2 declarations
ConeFullNormal.lean 1 declarations
ConeGraph.lean 22 declarations
ConeLetterCollapse.lean 12 declarations
ConeMappedWalk.lean 5 declarations
ConePresentationGroup.lean 11 declarations
ConeSkeleton.lean 15 declarations
ConeTopCollapse.lean 11 declarations
ConeTopGroup.lean 5 declarations
ConeWalkTarget.lean 22 declarations
ConnectedLevels.lean 3 declarations
ContactCapacity.lean 6 declarations
CoreFan.lean 12 declarations
CoreWordGraph.lean 17 declarations
Cost.lean 9 declarations
CouplingError.lean 2 declarations
CoverBoundary.lean 3 declarations
CubicalHomotopyExtension.lean 30 declarations
CycleCount.lean 7 declarations
CycleDecomposition.lean 14 declarations
CyclicLink.lean 28 declarations
CyclicTriangleBoundary.lean 22 declarations
CyclicTriangleCochains.lean 9 declarations
DevelopmentCATZero.lean 1 declarations
DevelopmentDeck.lean 12 declarations
DevelopmentGeodesic.lean 11 declarations
DevelopmentGeometricAction.lean 3 declarations
DevelopmentProper.lean 3 declarations
DevelopmentRadial.lean 7 declarations
Deviation.lean 6 declarations
DiagonalSampling.lean 6 declarations
DiagramSampling.lean 5 declarations
DipoleChain.lean 5 declarations
DipoleRemove.lean 14 declarations
DipoleStepChain.lean 1 declarations
DipoleSwitch.lean 5 declarations
Distinct.lean 4 declarations
EdgeChain.lean 14 declarations
EdgeContraction.lean 6 declarations
EdgeCoordinates.lean 4 declarations
EdgeErase.lean 5 declarations
EdgeEraseBoundary.lean 5 declarations
EdgeEraseComponents.lean 2 declarations
EdgeEraseCount.lean 2 declarations
EdgeEraseGenus.lean 2 declarations
EdgeMerge.lean 16 declarations
EdgeMergeComponents.lean 12 declarations
ElementaryCone.lean 24 declarations
ElementaryCover.lean 7 declarations
Exceptional.lean 13 declarations
ExtensionConditioning.lean 7 declarations
ExtensionMargin.lean 10 declarations
ExteriorTarget.lean 8 declarations
FaceChainSelection.lean 5 declarations
FaceSplice.lean 7 declarations
FaceSplit.lean 4 declarations
FaceWalk.lean 6 declarations
FanActivation.lean 3 declarations
FanApex.lean 35 declarations
FanRoute.lean 10 declarations
FiberLaw.lean 5 declarations
FiniteFanData.lean 14 declarations
FiniteFlatFacets.lean 3 declarations
FiniteLaw.lean 21 declarations
FiniteMassTransfer.lean 5 declarations
FinitePolygonModel.lean 27 declarations
FinitePolygonVoltage.lean 22 declarations
FinitePolyhedron.lean 16 declarations
FinitePolyhedronDeck.lean 10 declarations
FinitePolyhedronEdgePaths.lean 9 declarations
FinitePolyhedronLocal.lean 13 declarations
FinitePolyhedronMonodromy.lean 21 declarations
FinitePolyhedronPathAlgebra.lean 16 declarations
FinitePolyhedronPaths.lean 13 declarations
FinitePolyhedronVoltage.lean 12 declarations
FiniteSampling.lean 8 declarations
FiniteSelection.lean 5 declarations
Fragment.lean 19 declarations
FragmentSlots.lean 8 declarations
FrozenCancel.lean 1 declarations
FrozenFaceSide.lean 6 declarations
FrozenPrevious.lean 4 declarations
FrozenSideExists.lean 2 declarations
FrozenWalk.lean 12 declarations
FullWalkNormal.lean 2 declarations
GeneralSwitch.lean 5 declarations
GenericMoment.lean 4 declarations
GenericTable.lean 14 declarations
GeometricAction.lean 33 declarations
GeometricSpaceTransport.lean 4 declarations
GlobalClosedPicture.lean 2 declarations
Graph.lean 38 declarations
GraphAction.lean 17 declarations
GraphGroupWalk.lean 9 declarations
GraphLimit.lean 6 declarations
GraphSeparatorTransfer.lean 2 declarations
GraphSquares.lean 7 declarations
GraphSubpairing.lean 5 declarations
GraphSubstitution.lean 4 declarations
GraphWordFilling.lean 8 declarations
HSpaceFundamental.lean 10 declarations
HSpacePathObstruction.lean 10 declarations
IncidenceTemplate.lean 11 declarations
IndexedBoundaryPullback.lean 1 declarations
IndexedDiskUniqueness.lean 2 declarations
IndexedFace.lean 9 declarations
IndexedFanCards.lean 10 declarations
IndexedFanCounts.lean 25 declarations
IndexedFillingValue.lean 736 declarations
IndexedPayment.lean 3 declarations
IndexedPictureAppend.lean 4 declarations
IndexedPictureBasic.lean 9 declarations
IndexedPictureClosed.lean 6 declarations
IndexedPictureExistence.lean 5 declarations
IndexedPictureFold.lean 3 declarations
IndexedPictureReduction.lean 3 declarations
IndexedWordPicture.lean 9 declarations
IntegralCellularBoundary.lean 12 declarations
InvolutionPairs.lean 4 declarations
LeafFiber.lean 6 declarations
LeafMargin.lean 8 declarations
LetterCover.lean 10 declarations
LetterFillingArea.lean 1 declarations
LetterNormalPicture.lean 2 declarations
LiftedBasis.lean 13 declarations
LiftedClosedPicture.lean 3 declarations
LiftedDiagramSampling.lean 7 declarations
LinkApex.lean 12 declarations
LocalGeodesic.lean 1 declarations
LocalGeodesicContraction.lean 9 declarations
LocalGeodesicCover.lean 27 declarations
LocalGeodesicDistance.lean 14 declarations
LocalGeodesicLength.lean 4 declarations
LocalGeodesicRebase.lean 10 declarations
LocalGeodesicTopology.lean 6 declarations
LocalSegmentContinuation.lean 2 declarations
LocalSegmentTools.lean 4 declarations
LocalWeightedRank.lean 3 declarations
LoopSpaceReversal.lean 4 declarations
MacroCertificate.lean 63 declarations
MacroCycle.lean 7 declarations
MacroExceptional.lean 6 declarations
MacroFaceFilling.lean 2 declarations
MacroGroup.lean 8 declarations
MacroRadialIndex.lean 4 declarations
MacroWalk.lean 5 declarations
Main.lean 1 declarations
MappedCancellation.lean 1 declarations
MappedPicture.lean 5 declarations
MergeWalk.lean 8 declarations
MetricHexagon.lean 63 declarations
MetricProduct.lean 48 declarations
Moment.lean 15 declarations
NormalCell.lean 7 declarations
NormalDiskArea.lean 3 declarations
NormalFaceFilling.lean 3 declarations
Normalization.lean 8 declarations
Occurrence.lean 4 declarations
OneFaceFilling.lean 1 declarations
OrbitLimit.lean 18 declarations
OriginalLinearFilling.lean 2 declarations
OutsideComponentFilling.lean 1 declarations
PairingForest.lean 10 declarations
PairingTreeCotree.lean 2 declarations
ParameterizedSquareFilling.lean 10 declarations
Parity.lean 17 declarations
PathHomotopyTopology.lean 6 declarations
PathInSet.lean 3 declarations
PathLocalToGlobal.lean 3 declarations
PermErase.lean 10 declarations
PermErasePair.lean 10 declarations
PermEuler.lean 11 declarations
PermSwitch.lean 17 declarations
PictureBFSSeparator.lean 2 declarations
PictureBoundaryHull.lean 1 declarations
PictureBoundaryParity.lean 2 declarations
PictureComponentGraph.lean 13 declarations
PictureContact.lean 13 declarations
PictureCotreeColor.lean 10 declarations
PictureCotreeTree.lean 2 declarations
PictureDual.lean 8 declarations
PictureEuler.lean 7 declarations
PictureFaceCorners.lean 2 declarations
PictureFillingAlgebra.lean 3 declarations
PictureFullSeparator.lean 3 declarations
PictureGenus.lean 10 declarations
PictureLeaf.lean 3 declarations
PictureMap.lean 9 declarations
PictureMapFurther.lean 8 declarations
PictureMirror.lean 7 declarations
PictureOutsideColor.lean 7 declarations
PicturePartition.lean 9 declarations
PicturePlanarSeparator.lean 2 declarations
PictureRadiusSeparator.lean 1 declarations
PictureRestrict.lean 2 declarations
PictureRootSeparator.lean 1 declarations
PictureSqrtSeparator.lean 1 declarations
PictureStarGraph.lean 5 declarations
PictureSum.lean 9 declarations
PictureTriangulation.lean 17 declarations
PictureTriangulationEuler.lean 13 declarations
PictureUnderlyingGraph.lean 13 declarations
PictureVertexBoundary.lean 8 declarations
PictureVertexCut.lean 2 declarations
Pinned.lean 16 declarations
PlanarEdgeOrdering.lean 7 declarations
PlanarFacePartition.lean 1 declarations
PlanarPartitionBridge.lean 4 declarations
PlanarSubpairing.lean 6 declarations
PolygonBoundaryList.lean 9 declarations
PolygonContraction.lean 13 declarations
PolygonCornerPrimitive.lean 2 declarations
PolygonDiskProducer.lean 2 declarations
PolygonFilling.lean 2 declarations
PolygonLiftedCochain.lean 10 declarations
PolygonSphere.lean 2 declarations
PolygonSphereFurther.lean 12 declarations
PolygonTarget.lean 17 declarations
PolygonTriangleCochains.lean 12 declarations
PolygonTriangles.lean 6 declarations
Polygons.lean 9 declarations
Presentation.lean 28 declarations
PresentationDisk.lean 13 declarations
PrismConcat.lean 8 declarations
ProtectedNormal.lean 6 declarations
QuotientSum.lean 5 declarations
Random.lean 26 declarations
RankCollection.lean 22 declarations
RankSampling.lean 7 declarations
RankSelection.lean 4 declarations
RelativeApexAggregate.lean 3 declarations
RelativeApexLocal.lean 20 declarations
RelativeApexProducer.lean 6 declarations
RelativeContact.lean 20 declarations
RelativeDegree.lean 5 declarations
RelativeExceptional.lean 2 declarations
RelativeFaceCounts.lean 15 declarations
RelativeFaceSide.lean 6 declarations
RelativeFanCapacity.lean 2 declarations
RelativeFanLink.lean 21 declarations
RelativeFragment.lean 6 declarations
RelativeFrozenSide.lean 1 declarations
RelativeGlobalStep.lean 2 declarations
RelativeInstanceAt.lean 1 declarations
RelativeInteriorCount.lean 5 declarations
RelativeLayers.lean 5 declarations
RelativeMacroPolygon.lean 1 declarations
RelativeMultiplicity.lean 9 declarations
RelativePartition.lean 9 declarations
RelativePartitionEstimate.lean 12 declarations
RelativePayment.lean 10 declarations
RelativeRadialBoundary.lean 16 declarations
RelativeRawAccount.lean 2 declarations
RelativeRawCount.lean 10 declarations
RelativeRawPosition.lean 4 declarations
RelativeSlots.lean 8 declarations
RelativeSmallPartition.lean 1 declarations
RelativeTopTurns.lean 7 declarations
RelativeTriangleTransport.lean 14 declarations
RelativeTurnTransport.lean 5 declarations
RelativeWeights.lean 4 declarations
RestrictOccurrence.lean 24 declarations
SamplingStage.lean 13 declarations
SelectedPresentation.lean 13 declarations
Selection.lean 5 declarations
SeparatorBudget.lean 5 declarations
SeparatorComponents.lean 1 declarations
SeparatorCutoff.lean 2 declarations
SeparatorDecomposition.lean 2 declarations
SeparatorGrouping.lean 2 declarations
SeparatorRecursion.lean 17 declarations
SetoidGlue.lean 9 declarations
SetoidRestrict.lean 2 declarations
Shape.lean 14 declarations
ShortSegmentLift.lean 3 declarations
SimpleLetterPresentation.lean 8 declarations
SimplexCoordinates.lean 9 declarations
SixCounts.lean 16 declarations
SixRows.lean 8 declarations
SmallSimplexCoordinates.lean 9 declarations
SquareBoundaryExtension.lean 14 declarations
SquarePathFilling.lean 31 declarations
StarActual.lean 4 declarations
StarBudget.lean 9 declarations
StarCoupling.lean 7 declarations
StarError.lean 8 declarations
StarFiber.lean 12 declarations
StarIncidence.lean 16 declarations
StarMean.lean 9 declarations
StarModel.lean 17 declarations
StarModelFurther.lean 1 declarations
StarRate.lean 8 declarations
StarVariance.lean 10 declarations
StationaryInterpolation.lean 9 declarations
StepChain.lean 1 declarations
SubpairingCopies.lean 7 declarations
SubpairingDarts.lean 3 declarations
SubpairingGraph.lean 5 declarations
SubpairingTree.lean 3 declarations
TableSelection.lean 5 declarations
TangentCone.lean 47 declarations
TangentRay.lean 47 declarations
Template.lean 45 declarations
Test.lean 13 declarations
TreeCentroid.lean 2 declarations
TreeCentroidComponents.lean 3 declarations
TreeCentroidCut.lean 3 declarations
TreeHull.lean 4 declarations
TreePathDepth.lean 2 declarations
TreePathHull.lean 8 declarations
TreePathIntDepth.lean 3 declarations
TreeSubpairingLift.lean 1 declarations
TriangleCoordinates.lean 5 declarations
TriangleEdgeIntersection.lean 1 declarations
TriangleHomotopyExtension.lean 14 declarations
TriangleSquare.lean 18 declarations
TriangleSquareFurther.lean 3 declarations
UniformGeodesicProper.lean 1 declarations
UniformMetricCover.lean 21 declarations
VoltageCellGluing.lean 6 declarations
VoltageClosedCells.lean 17 declarations
VoltageEdgeAgreement.lean 7 declarations
VoltageEdgeCorrection.lean 11 declarations
VoltageEdges.lean 12 declarations
VoltageFacePrisms.lean 9 declarations
VoltageGraphHomotopy.lean 10 declarations
VoltagePrismGluing.lean 12 declarations
VoltageTriangleContraction.lean 19 declarations
VoltageTriangleHomotopy.lean 13 declarations
VoltageTriangles.lean 9 declarations
WalkApexAggregate.lean 3 declarations
WalkCancel.lean 9 declarations
WalkCell.lean 14 declarations
WalkClasses.lean 18 declarations
WalkConeLink.lean 5 declarations
WalkCover.lean 11 declarations
WalkFacePosition.lean 5 declarations
WalkFanCapacity.lean 2 declarations
WalkFanCorner.lean 9 declarations
WalkFanIncoming.lean 5 declarations
WalkFragment.lean 22 declarations
WalkInstanceAt.lean 1 declarations
WalkMultiplicity.lean 10 declarations
WalkNormal.lean 3 declarations
WalkPayment.lean 10 declarations
WalkRadial.lean 3 declarations
WalkRadialBoundary.lean 16 declarations
WalkRawPosition.lean 12 declarations
WalkTopTurns.lean 7 declarations
WalkTriangleTransport.lean 14 declarations
WalkTurnTransport.lean 5 declarations
WeightedCoincidence.lean 13 declarations
WeightedRank.lean 4 declarations
WordDisk.lean 18 declarations
WordPicture.lean 8 declarations
WordPictureAppend.lean 4 declarations
WordPictureArea.lean 2 declarations
WordPictureBase.lean 4 declarations
WordPictureCell.lean 6 declarations
WordPictureExist.lean 7 declarations
WordPictureFilling.lean 1 declarations
WordPictureFold.lean 4 declarations
WordPictureLiteral.lean 5 declarations
WordPictureMarked.lean 1 declarations
WordPicturePeel.lean 2 declarations
WordSubstitution.lean 4 declarations