`OAI/Combinatorics/Crossing/`

1494 declarations, 0 contain sorry, 0 declared as axioms; 339 files

Files

AdaptedFamily.lean 1 declarations
AdditiveBlockRelation.lean 2 declarations
AdjacentSurgeryDrawing.lean 7 declarations
AdjacentSurgeryPointRemoval.lean 3 declarations
AdjacentSurgeryRoutes.lean 6 declarations
AdmissibleAdjacentSurgery.lean 1 declarations
AffineIntervalRestriction.lean 3 declarations
AffinePathHalves.lean 9 declarations
AffineSideEvents.lean 7 declarations
AffineSubdivisionRefinement.lean 2 declarations
AlternatingPaths.lean 3 declarations
ArcRangeMinimality.lean 1 declarations
AssembledAdmissibleDrawing.lean 4 declarations
AssembledContinuousDrawing.lean 6 declarations
AssembledCrossings.lean 5 declarations
AssembledEdge.lean 8 declarations
AssembledNoTriples.lean 1 declarations
AssembledPortIncidence.lean 4 declarations
AxisAdmissibility.lean 4 declarations
AxisConcurrency.lean 6 declarations
AxisContinuousDrawing.lean 4 declarations
AxisCrossingOrder.lean 5 declarations
AxisFiniteCrossings.lean 5 declarations
AxisGenericPositions.lean 2 declarations
AxisSegments.lean 8 declarations
BalancedAxisCrossingCount.lean 6 declarations
BalancedAxisDrawing.lean 15 declarations
BalancedAxisIntervals.lean 8 declarations
BalancedRayPairs.lean 9 declarations
BipartiteDartGeometry.lean 12 declarations
Bivariate.lean 18 declarations
BivariateCoefficients.lean 6 declarations
BoundaryCollar.lean 1 declarations
ChainPieceInteriors.lean 1 declarations
ChainTracePieces.lean 3 declarations
ChordEdgeIntersections.lean 1 declarations
ChordExteriorSeparation.lean 3 declarations
ChordOrientations.lean 4 declarations
ChordPairing.lean 8 declarations
ChordTransversality.lean 3 declarations
CircleChords.lean 10 declarations
CircleConnectors.lean 6 declarations
CircleDeterminantOrder.lean 3 declarations
CircleOffset.lean 4 declarations
CircleOffsetLine.lean 5 declarations
CircleOffsetParameter.lean 5 declarations
CircleParameterChart.lean 3 declarations
ClosedPolygonIntersection.lean 1 declarations
CollinearSegmentUnion.lean 1 declarations
CompactCorridors.lean 1 declarations
ConeIntersection.lean 1 declarations
ConnectorOtherDisks.lean 1 declarations
ConnectorSupportingLines.lean 8 declarations
ConnectorTrackAvoidance.lean 2 declarations
ConstructAdjacentSurgery.lean 1 declarations
CrossingCoordinates.lean 9 declarations
CrossingCutWalks.lean 2 declarations
CrossingDiskCount.lean 5 declarations
CrossingDiskIncidence.lean 8 declarations
CrossingDiskNeighborhood.lean 7 declarations
CrossingDiskOwners.lean 3 declarations
CrossingDiskUniqueness.lean 6 declarations
CrossingIncidence.lean 9 declarations
CrossingPortClearance.lean 3 declarations
CrossingReconnection.lean 3 declarations
CrossingSurgeryGraph.lean 4 declarations
CurveDiskIsolation.lean 1 declarations
CutTraceSeparation.lean 7 declarations
CutVertexAvoidance.lean 5 declarations
CycleBlockIntersections.lean 4 declarations
CycleEndpointSum.lean 3 declarations
CycleMatrixBlocks.lean 7 declarations
CyclePairing.lean 1 declarations
CyclicSumArithmetic.lean 3 declarations
CyclicWalkDarts.lean 8 declarations
DartCyclePaths.lean 14 declarations
DartPairIntersections.lean 4 declarations
DartPathRealizations.lean 8 declarations
DegreeCounting.lean 3 declarations
DeletionCount.lean 3 declarations
DetectorAnnihilation.lean 4 declarations
DetectorCrossingBound.lean 3 declarations
DetectorRank.lean 4 declarations
DetectorRelabeling.lean 6 declarations
DiskFillingContainment.lean 7 declarations
DiskPassage.lean 7 declarations
DiskSegments.lean 4 declarations
DrawingDefinition.lean 12 declarations
DrawingDeletion.lean 5 declarations
DrawingDiskIsolation.lean 2 declarations
DrawingEdgeWalk.lean 6 declarations
DrawingEdgeWalkTrace.lean 2 declarations
DrawingExteriorReplacement.lean 1 declarations
DrawingMarks.lean 8 declarations
DrawingPassages.lean 2 declarations
DrawingPorts.lean 8 declarations
DrawingRangeCrossings.lean 4 declarations
DrawingRestriction.lean 7 declarations
DrawingSegmentIncidence.lean 6 declarations
DrawingSpokePorts.lean 8 declarations
DrawingSubdivisionGraph.lean 5 declarations
DrawingVertexPlacement.lean 5 declarations
DrawingWalkCutTraces.lean 3 declarations
DrawnEdgeChains.lean 8 declarations
EmbeddedGraphPaths.lean 5 declarations
EndpointFlagPairing.lean 13 declarations
EndpointVisits.lean 2 declarations
EvaluationAmbient.lean 9 declarations
EvenCrossingLowerBound.lean 2 declarations
ExpectedTrackGeometry.lean 1 declarations
ExteriorArcReplacement.lean 1 declarations
ExteriorChordMeeting.lean 2 declarations
ExteriorCrossingCut.lean 6 declarations
ExteriorSegmentGraph.lean 7 declarations
ExteriorSpokeMeeting.lean 1 declarations
ExtraDrawingSubdivision.lean 2 declarations
FiniteAffineCover.lean 7 declarations
FiniteCircleCoordinates.lean 2 declarations
FiniteConePoint.lean 1 declarations
FiniteDiskCollar.lean 4 declarations
FiniteEventualRadius.lean 1 declarations
FiniteIntersectionDrawing.lean 6 declarations
FiniteLineAvoidance.lean 4 declarations
FiniteMovingPoints.lean 1 declarations
FinitePathChain.lean 3 declarations
FinitePolygonalComposition.lean 6 declarations
FiniteScaledRadius.lean 1 declarations
FiniteSeparation.lean 2 declarations
FirstLastVisits.lean 1 declarations
FloorArithmetic.lean 6 declarations
FourCyclePairing.lean 3 declarations
FourCycles.lean 6 declarations
GeneralOrderAveraging.lean 2 declarations
GeneralSpokeAveraging.lean 3 declarations
GenericPointExtension.lean 1 declarations
GenericPointFamily.lean 1 declarations
GenericPolygonIntersection.lean 2 declarations
GenericPolynomialBox.lean 1 declarations
GlobalCycleAveraging.lean 2 declarations
GlobalCycleIntersection.lean 1 declarations
GraphSequenceWalk.lean 4 declarations
GraphWalkRealizationLaws.lean 5 declarations
GraphWalkTrace.lean 5 declarations
HalfOrderInvertibility.lean 2 declarations
HalfOrderReduction.lean 8 declarations
IncidentSpokePorts.lean 7 declarations
IndexedMatrixRankSum.lean 2 declarations
InnerDrawingPassages.lean 16 declarations
Interpolation.lean 13 declarations
IntervalSegmentStrict.lean 1 declarations
IntervalSegments.lean 2 declarations
LocalLineBends.lean 2 declarations
LocalSegmentTransversality.lean 2 declarations
LocallyStraightNormalization.lean 4 declarations
LocallyTransverseNormalization.lean 4 declarations
Main.lean 3 declarations
MarkedCurveDisks.lean 2 declarations
MatrixGraphs.lean 3 declarations
MatrixRankBounds.lean 4 declarations
MatrixRankSum.lean 2 declarations
MiddleEdgeIncidence.lean 3 declarations
MiddlePathInjective.lean 2 declarations
MiddleSpokeMeeting.lean 6 declarations
MinimumChainGeometry.lean 4 declarations
MinimumChainVertexPieces.lean 2 declarations
MovingDiskClearance.lean 2 declarations
MovingSegmentStability.lean 3 declarations
NoAdjacentLocalNormalization.lean 1 declarations
NoAdjacentNormalization.lean 2 declarations
NodeMoments.lean 6 declarations
NodeRankLoss.lean 2 declarations
NormalOffsetExterior.lean 4 declarations
NormalizedPolygonalDrawing.lean 2 declarations
OddCrossingLowerBound.lean 1 declarations
OddNormalizedLowerBound.lean 1 declarations
OffsetBendSegments.lean 3 declarations
OffsetSegments.lean 4 declarations
OffsetTrack.lean 6 declarations
OffsetVectors.lean 8 declarations
OpenSegmentEndpoints.lean 2 declarations
OrderShift.lean 3 declarations
OrderedAffineSubdivision.lean 2 declarations
OrderedCrossingPorts.lean 4 declarations
OrderedExteriorPaths.lean 14 declarations
OrderedKnotCover.lean 2 declarations
OrderedNodeIndices.lean 11 declarations
OrderedPassages.lean 6 declarations
OrderedPathParts.lean 9 declarations
OrientedSimilarity.lean 6 declarations
ParallelDirection.lean 5 declarations
ParameterNeighborhoods.lean 5 declarations
PathConcatenationInjective.lean 2 declarations
PathEndpointNeighborhoods.lean 1 declarations
PathSubarc.lean 5 declarations
PeriodicPolygon.lean 7 declarations
PhysicalCircleAveraging.lean 2 declarations
PhysicalSpokeAveraging.lean 1 declarations
PhysicalVertexChords.lean 2 declarations
PlanarDeterminant.lean 9 declarations
PlanarSegments.lean 12 declarations
PolygonComposition.lean 7 declarations
PolygonStability.lean 1 declarations
PolygonTransversalityStability.lean 1 declarations
PolygonalArcInjective.lean 4 declarations
PolygonalBoundaryReplacement.lean 3 declarations
PolygonalChainComposition.lean 5 declarations
PolygonalChainExistence.lean 4 declarations
PolygonalChainOperations.lean 9 declarations
PolygonalChainShortcuts.lean 5 declarations
PolygonalChainTransversality.lean 5 declarations
PolygonalChains.lean 7 declarations
PolygonalEndpointCasts.lean 3 declarations
PolygonalExterior.lean 5 declarations
PolygonalNormalization.lean 5 declarations
PolygonalParametrization.lean 9 declarations
PolygonalParametrizationCover.lean 1 declarations
PolygonalReach.lean 5 declarations
PolygonalWalks.lean 6 declarations
PolynomialCoordinates.lean 7 declarations
PolynomialFiltration.lean 9 declarations
PolynomialKernel.lean 27 declarations
PolynomialLinearMatrix.lean 3 declarations
PolynomialMinors.lean 5 declarations
ProperCrossingLocality.lean 3 declarations
ProperSegmentCrossing.lean 1 declarations
RadialBoundaryPorts.lean 8 declarations
RadialExterior.lean 5 declarations
RankDetector.lean 8 declarations
RankMultiplicity.lean 2 declarations
RankSpecialization.lean 3 declarations
ReconnectedIntersectionCases.lean 2 declarations
ReconnectedPaths.lean 8 declarations
ReconnectedPointRemoval.lean 1 declarations
ReconnectedVertexAvoidance.lean 5 declarations
ReconnectedWalks.lean 6 declarations
ReconnectionAvoidance.lean 3 declarations
ReconnectionChords.lean 7 declarations
ReconnectionOppositeCuts.lean 4 declarations
ReconnectionOtherEdges.lean 3 declarations
ReconnectionVertexAvoidance.lean 2 declarations
RectangleAlgebra.lean 7 declarations
ReducedCrossingCorners.lean 6 declarations
ReducedCrossingTransversality.lean 2 declarations
ReducedPolygonalPresentation.lean 3 declarations
ReplaceDrawingEdges.lean 5 declarations
ReplaceDrawingRangeCases.lean 1 declarations
RetainedArcDisjointness.lean 1 declarations
RetainedDrawingArcs.lean 16 declarations
RoundCircleChords.lean 4 declarations
RoundDiskChords.lean 2 declarations
RoundDiskClearance.lean 4 declarations
RoundDiskVisits.lean 3 declarations
RowCrossingCount.lean 6 declarations
SegmentAffineForms.lean 2 declarations
SegmentAugmentation.lean 6 declarations
SegmentClosedIncidence.lean 2 declarations
SegmentContinuity.lean 6 declarations
SegmentCrossingCoordinates.lean 4 declarations
SegmentIntersectionUnique.lean 1 declarations
SegmentParameters.lean 4 declarations
SegmentSides.lean 7 declarations
SegmentSymmetries.lean 6 declarations
SegmentTraversalReversal.lean 6 declarations
SharedTrackAvoidance.lean 1 declarations
ShiftedEdgeIntersections.lean 1 declarations
ShiftedRadialPieces.lean 2 declarations
ShiftedSegmentStability.lean 5 declarations
ShiftedTrackDisks.lean 2 declarations
ShortVertexRadius.lean 1 declarations
SimilarityCoordinates.lean 6 declarations
SimultaneousExteriorArcs.lean 1 declarations
SimultaneousPolygonalReplacement.lean 2 declarations
SortedMarkedParameters.lean 2 declarations
SortedSideEvents.lean 3 declarations
SpokeEndpointSeparation.lean 4 declarations
SpokePieceIsolation.lean 2 declarations
SpokeTrackDirections.lean 4 declarations
StageDegreeBound.lean 2 declarations
StepEvents.lean 3 declarations
StraightChainIntersections.lean 6 declarations
StraightChainTransversality.lean 2 declarations
SubdivisionPointEndpoints.lean 2 declarations
SubdivisionSegments.lean 6 declarations
SublevelExtrema.lean 1 declarations
SubspaceIntersection.lean 2 declarations
SubspaceProjection.lean 2 declarations
SurgeryCrossingContainment.lean 1 declarations
SurgeryCutWalks.lean 4 declarations
SurgeryFiniteDrawing.lean 2 declarations
SurgeryNoTriples.lean 1 declarations
SurgeryPathWitnesses.lean 4 declarations
SurgeryRouteIntersections.lean 4 declarations
SurgeryStrictPointCount.lean 2 declarations
TangentTrackIdentity.lean 6 declarations
TrackChordSeparation.lean 2 declarations
TrackEndpointConnections.lean 8 declarations
TransversalityStability.lean 3 declarations
TransversePolygonIntersection.lean 2 declarations
TriangleEntryExit.lean 6 declarations
TriangleFactorization.lean 5 declarations
TriangleOrientations.lean 7 declarations
TriangleSideEvent.lean 4 declarations
TriangleTransversality.lean 6 declarations
TruncatedChainDirections.lean 6 declarations
TruncatedChainPath.lean 3 declarations
TruncatedChainVertices.lean 9 declarations
TruncatedCrossingCorners.lean 1 declarations
TruncatedCrossingRetention.lean 1 declarations
TruncatedDrawingDisks.lean 2 declarations
TruncatedDrawingInteriors.lean 2 declarations
TruncatedRadialDots.lean 5 declarations
TruncatedRadialEnds.lean 3 declarations
TruncatedSegmentTransversality.lean 2 declarations
TruncatedSignedIntersections.lean 7 declarations
TruncatedSpokeCoordinates.lean 9 declarations
TruncatedSpokeDirections.lean 12 declarations
TruncatedTraceDecomposition.lean 2 declarations
TruncatedTrackAvoidance.lean 2 declarations
TruncatedTrackStability.lean 1 declarations
TwoTriangleBasis.lean 8 declarations
TwoTriangleIndices.lean 15 declarations
TwoTriangleUnisolvence.lean 3 declarations
UniformCrossTypeGeometry.lean 1 declarations
UniformSpokeRadii.lean 4 declarations
UniformTrackPerturbation.lean 2 declarations
UniqueWalkPassage.lean 4 declarations
VertexChordIntersections.lean 2 declarations
VertexDiskSpokes.lean 3 declarations
VertexDisksCrossingFree.lean 1 declarations
VertexEndpointPorts.lean 7 declarations
VertexOrderDetector.lean 7 declarations
VertexPassagePairing.lean 4 declarations
VertexPieceClearance.lean 1 declarations
VertexSpokeBounds.lean 2 declarations
VertexTraceDisks.lean 1 declarations
VertexTruncation.lean 13 declarations
VertexTruncationGeometry.lean 6 declarations
WalkVectorSum.lean 6 declarations
WeightedGram.lean 2 declarations