OAI/Topology/ArtinGroups/ParabolicIntersections/
1130 declarations, 0 contain sorry, 0 declared as axioms; 221 files
Files
- ActiveColors.lean 4 declarations
- AcyclicTwist.lean 4 declarations
- AcyclicTwistInput.lean 2 declarations
- AmalgamAcyclic.lean 7 declarations
- AmalgamGraph.lean 16 declarations
- AmalgamNoncommuting.lean 1 declarations
- AmalgamReduced.lean 3 declarations
- ArtinRelabel.lean 4 declarations
- AvoidingBoundaryRays.lean 2 declarations
- AvoidingRealization.lean 1 declarations
- Basic.lean 20 declarations
- BoundaryWitness.lean 3 declarations
- BraidRestriction.lean 2 declarations
- CoefficientPaths.lean 9 declarations
- ConditionalMain.lean 6 declarations
- ConnectedMinima.lean 8 declarations
- ConnectedSupport.lean 6 declarations
- Consequences.lean 8 declarations
- CosetContainment.lean 5 declarations
- CoxeterChainMinimum.lean 3 declarations
- CoxeterChainRoots.lean 3 declarations
- CoxeterProjectionSupport.lean 6 declarations
- DynamicsDefinitions.lean 11 declarations
- DynamicsEquivalence.lean 1 declarations
- DynamicsMain.lean 3 declarations
- DynamicsUnconditional.lean 1 declarations
- EmptyPlacement.lean 1 declarations
- FixedFactor.lean 3 declarations
- FoldingGcd.lean 2 declarations
- FoldingGcdInput.lean 2 declarations
- FoldingHead.lean 4 declarations
- FoldingPositive.lean 7 declarations
- FoldingSimpleGcd.lean 2 declarations
- GeneratorPowers.lean 9 declarations
- GraphMetric.lean 3 declarations
- GraphRealizationAction.lean 14 declarations
- GraphRealizationAcylindrical.lean 2 declarations
- GraphRealizationDistance.lean 23 declarations
- GraphRealizationGeodesic.lean 8 declarations
- GraphRealizationHyperbolic.lean 4 declarations
- GraphRealizationSpace.lean 17 declarations
- GraphWalkLevels.lean 1 declarations
- IncomingSpanning.lean 1 declarations
- InitialMinimum.lean 5 declarations
- LayerErasure.lean 1 declarations
- Main.lean 3 imports, no declarations
- MainIntersection.lean 9 declarations
- MeshAdjacent.lean 5 declarations
- MeshContraction.lean 6 declarations
- MeshGraphNilpotence.lean 7 declarations
- MeshGraphWeights.lean 3 declarations
- MeshInsertionMatrix.lean 1 declarations
- MeshMain.lean 4 declarations
- MeshMatrixAction.lean 8 declarations
- MeshNaturality.lean 7 declarations
- MeshNilpotence.lean 5 declarations
- MeshNormalization.lean 7 declarations
- MeshPathEvaluation.lean 7 declarations
- MeshPathSpaces.lean 6 declarations
- MeshPerron.lean 3 declarations
- MeshProjection.lean 9 declarations
- MeshProjectionAlgebra.lean 3 declarations
- MeshProjectionCutoff.lean 5 declarations
- MeshProjectionInduction.lean 4 declarations
- MeshQuantum.lean 8 declarations
- MeshQuiver.lean 8 declarations
- MeshQuiverAlgebra.lean 3 declarations
- MeshQuiverWords.lean 2 declarations
- MeshSpectralUpper.lean 1 declarations
- MeshTrace.lean 6 declarations
- MetricUnitCurves.lean 6 declarations
- NonCliqueDynamics.lean 2 declarations
- NoncommutingGraph.lean 3 declarations
- NormalParabolic.lean 6 declarations
- NormalizerAlgebra.lean 3 declarations
- NullBoundary.lean 1 declarations
- OrbitEdgeGraph.lean 10 declarations
- ParabolicCore.lean 4 declarations
- ParabolicCosetProjection.lean 15 declarations
- ParabolicMinimal.lean 1 declarations
- ParabolicMinimumStep.lean 2 declarations
- ParabolicProductProper.lean 3 declarations
- ParabolicRead.lean 9 declarations
- ParabolicReadBraid.lean 2 declarations
- ParabolicReadReduced.lean 4 declarations
- ParabolicRetractionAction.lean 9 declarations
- PathImages.lean 6 declarations
- PeriodicBoundary.lean 2 declarations
- PointedBlockBoundary.lean 1 declarations
- PointedBoundaryZero.lean 4 declarations
- PointedCandidate.lean 3 declarations
- PointedCandidateBlock.lean 2 declarations
- PointedCandidateCapped.lean 1 declarations
- PointedCandidateComparison.lean 1 declarations
- PointedCandidateFixed.lean 1 declarations
- PointedCandidateNumerical.lean 1 declarations
- PointedCap.lean 3 declarations
- PointedCapSaturation.lean 1 declarations
- PointedCappedCandidate.lean 5 declarations
- PointedCosetExteriorCap.lean 5 declarations
- PointedCosetGeometry.lean 3 declarations
- PointedCosetProduct.lean 4 declarations
- PointedFamily.lean 11 declarations
- PointedGroupProbeEuler.lean 1 declarations
- PointedInitialCounts.lean 4 declarations
- PointedInitialStabilizer.lean 2 declarations
- PointedMultiplicity.lean 8 declarations
- PointedMultiplicityZero.lean 2 declarations
- PointedNullObstruction.lean 1 declarations
- PointedNullPatch.lean 2 declarations
- PointedProbeCap.lean 2 declarations
- PointedProbeRaiseLower.lean 2 declarations
- PointedProfile.lean 16 declarations
- PointedResidueActive.lean 16 declarations
- PointedResidueActiveEmpty.lean 3 declarations
- PointedResidueAllowed.lean 11 declarations
- PointedResidueEarlierLower.lean 15 declarations
- PointedResidueEarlierLowerIso.lean 7 declarations
- PointedResidueHeightZero.lean 5 declarations
- PointedResidueRank.lean 15 declarations
- PointedResidueSingleOpen.lean 1 declarations
- PointedResidueZeroLower.lean 4 declarations
- PointedRows.lean 1 declarations
- PointedSpecialResidue.lean 2 declarations
- PointedSphericalNoChain.lean 3 declarations
- PointedStrictResidue.lean 3 declarations
- PointedTop.lean 2 declarations
- PointedTypeComponent.lean 8 declarations
- PointedWeighted.lean 4 declarations
- PositiveHeadProduct.lean 1 declarations
- PositiveSupport.lean 12 declarations
- PositiveTransport.lean 7 declarations
- ProperParabolicMalnormal.lean 2 declarations
- ProperPositiveSupport.lean 1 declarations
- RankReduction.lean 1 declarations
- ReducedDynamicsMain.lean 5 declarations
- ReducedInputsMain.lean 6 declarations
- ReducedPositiveExtension.lean 1 declarations
- RelativeActive.lean 2 declarations
- RelativeAllEligible.lean 5 declarations
- RelativeDescending.lean 4 declarations
- RelativeDiagram.lean 8 declarations
- RelativeEligible.lean 8 declarations
- RelativeEligibleBlocks.lean 4 declarations
- RelativeEligibleFactor.lean 4 declarations
- RelativeEligibleWithin.lean 10 declarations
- RelativeEmbedding.lean 1 declarations
- RelativeFamily.lean 13 declarations
- RelativeHeight.lean 20 declarations
- RelativeInitialStabilizer.lean 3 declarations
- RelativeInvisibleFactor.lean 6 declarations
- RelativeLowerBasics.lean 3 declarations
- RelativeLowerComparison.lean 4 declarations
- RelativeLowerConnected.lean 4 declarations
- RelativeLowerContractible.lean 3 declarations
- RelativeLowerRetraction.lean 13 declarations
- RelativeMinimumContainment.lean 7 declarations
- RelativeNullBlockData.lean 14 declarations
- RelativeNullLayer.lean 1 declarations
- RelativePeaks.lean 14 declarations
- RelativePoset.lean 10 declarations
- RelativeTieLower.lean 6 declarations
- RelativeTiedDescent.lean 5 declarations
- RelativeTies.lean 10 declarations
- RelativeTranslation.lean 11 declarations
- RelativeUpperBasics.lean 9 declarations
- RelativeUpperComparison.lean 5 declarations
- RelativeUpperConnected.lean 10 declarations
- RelativeUpperSigns.lean 11 declarations
- SphericalCochain.lean 7 declarations
- SphericalCommonExtension.lean 4 declarations
- SphericalGap.lean 3 declarations
- SphericalMesh.lean 7 declarations
- SphericalNoChain.lean 6 declarations
- SphericalProperSupport.lean 1 declarations
- SphericalReduction.lean 3 declarations
- StabilizerDescent.lean 7 declarations
- StandardEmbedding.lean 5 declarations
- TokenBoundary.lean 1 declarations
- TreeActionDefinitions.lean 4 declarations
- TreeAvoidingGraph.lean 6 declarations
- TreeBallCount.lean 3 declarations
- TreeBoundaryRays.lean 8 declarations
- TreeBranch.lean 4 declarations
- TreeBranchingHyperbolic.lean 3 declarations
- TreeBridge.lean 2 declarations
- TreeConvex.lean 3 declarations
- TreeConvexSupport.lean 2 declarations
- TreeFixedPaths.lean 5 declarations
- TreeInteriorImage.lean 1 declarations
- TreeInvariantTranslate.lean 2 declarations
- TreeMinimalNormal.lean 1 declarations
- TreeMinimalPair.lean 1 declarations
- TreePathMetric.lean 4 declarations
- TreePaths.lean 2 declarations
- TreePeriodicGrowth.lean 5 declarations
- TreePeriodicPaths.lean 13 declarations
- TreeSegmentBallCount.lean 2 declarations
- TreeSegmentCount.lean 4 declarations
- TreeSegmentOccurrences.lean 8 declarations
- TreeSeparatedPaths.lean 2 declarations
- TreeShortcutAcylindrical.lean 1 declarations
- TreeShortcutHyperbolic.lean 3 declarations
- TreeShortcutMetric.lean 4 declarations
- TreeShortcutPosition.lean 3 declarations
- TreeTranslationSegment.lean 6 declarations
- TreeTripod.lean 5 declarations
- UnconditionalMain.lean 6 declarations
- VisualAcylindrical.lean 1 declarations
- VisualAmalgam.lean 17 declarations
- VisualAmalgamProperties.lean 2 declarations
- VisualEdgeMalnormal.lean 1 declarations
- VisualEdgeTransitive.lean 1 declarations
- VisualFactorMalnormal.lean 5 declarations
- VisualInfiniteBranching.lean 2 declarations
- VisualNonVirtuallyCyclic.lean 3 declarations
- VisualParabolicSubtree.lean 6 declarations
- VisualTree.lean 14 declarations
- VisualTreeProperties.lean 3 declarations
- VisualTrivialSegment.lean 2 declarations
- WeakMalnormalAlgebra.lean 3 declarations