`OAI/Geometry/SurfaceImmersion/Whitney/`

768 declarations, 0 contain sorry, 0 declared as axioms; 300 files

Files

ActualProfileCollar.lean 4 declarations
ActualRelativeFrame.lean 2 declarations
ActualRuledCrosscapStrip.lean 1 declarations
ActualRuledRectangle.lean 2 declarations
ActualRuledTargetTube.lean 1 declarations
ActualRuledTwist.lean 1 declarations
ActualSurfaceCollarFamily.lean 1 declarations
ActualSurfaceCollarProfiles.lean 1 declarations
AdaptedDoubleSheetModels.lean 3 declarations
AdvancingCornerArc.lean 1 declarations
AdvancingCornerParameters.lean 1 declarations
ArcDensityLocal.lean 1 declarations
ArcJoinOrientation.lean 1 declarations
ArcTimeChartPartition.lean 2 declarations
ArcTimeGermPartition.lean 1 declarations
ArcVertexCoordinates.lean 1 declarations
AxisCollarJet.lean 1 declarations
BoundaryInvariantCollar.lean 3 declarations
CalibratedCollarData.lean 2 declarations
CalibratedCollarFamily.lean 1 declarations
CenteredCrosscapPreparation.lean 5 declarations
CircularBoundaryArcs.lean 10 declarations
CleanCrosscapNeighborhoods.lean 1 declarations
CleanSurfacePairs.lean 4 declarations
ClosedArcHalfChart.lean 1 declarations
ClosedDoubleArcLift.lean 2 declarations
CollarDensityMoments.lean 7 declarations
CollarVelocity.lean 18 declarations
CollarVelocityAngle.lean 12 declarations
CollarVelocityCalibration.lean 5 declarations
CollarVelocityClock.lean 8 declarations
CollarVelocityFamily.lean 4 declarations
CollarVelocityInverse.lean 12 declarations
CollarVelocityMean.lean 8 declarations
CollarVelocityPeriod.lean 17 declarations
CollarVelocityReparam.lean 13 declarations
CollarVelocityTurns.lean 7 declarations
CollarVelocityVector.lean 6 declarations
CompactArcJoin.lean 2 declarations
CompactArcLastIntersection.lean 2 declarations
CompactArcLocalNeighborhood.lean 1 declarations
CompactArcSubdivision.lean 1 declarations
CompactArcTimeChart.lean 1 declarations
CompactCleanPairRegularization.lean 1 declarations
CompactCollarJet.lean 1 declarations
CompactCollarPositivity.lean 2 declarations
CompactCrosscapIsolation.lean 1 declarations
CompactCurveArc.lean 3 declarations
CompactDoublePairs.lean 4 declarations
CompactExactCollar.lean 1 declarations
CompactFramedCurveTube.lean 2 declarations
CompactPairC1Regularization.lean 1 declarations
CompactPairRegularization.lean 1 declarations
CompactRelativePairRegularization.lean 1 declarations
CompactSurfacePairStability.lean 1 declarations
CompactifiedDoubleCurve.lean 5 declarations
ConstructedCollarFamily.lean 1 declarations
ControlledCollarLoop.lean 1 declarations
CornerArcSeparation.lean 2 declarations
CornerBridgeEmbedding.lean 1 declarations
CornerBridgePath.lean 14 declarations
CornerChartReflection.lean 9 declarations
CornerGraphSeparation.lean 5 declarations
CornerParameterOrientation.lean 6 declarations
CrosscapArcCoordinates.lean 1 declarations
CrosscapArcEndpoint.lean 1 declarations
CrosscapArcGermRestriction.lean 1 declarations
CrosscapArcNeighborhood.lean 2 declarations
CrosscapAxisCoordinates.lean 3 declarations
CrosscapAxisCurve.lean 6 declarations
CrosscapAxisDoublePair.lean 1 declarations
CrosscapAxisEndpointGerms.lean 1 declarations
CrosscapAxisFactor.lean 1 declarations
CrosscapAxisFinishGerm.lean 1 declarations
CrosscapAxisImageVelocity.lean 2 declarations
CrosscapAxisStartGerm.lean 1 declarations
CrosscapCancellationHeight.lean 4 declarations
CrosscapChartTransition.lean 1 declarations
CrosscapCompactArc.lean 1 declarations
CrosscapComposedDirection.lean 1 declarations
CrosscapConnectingArc.lean 2 declarations
CrosscapCoordinateRegularity.lean 2 declarations
CrosscapCoordinateStrip.lean 2 declarations
CrosscapCutoffBounds.lean 2 declarations
CrosscapDerivativeNonzero.lean 1 declarations
CrosscapDiagonalClosure.lean 1 declarations
CrosscapDisjointCharts.lean 1 declarations
CrosscapDoubleRay.lean 4 declarations
CrosscapEndArcs.lean 2 declarations
CrosscapEndpoint.lean 1 declarations
CrosscapEndpointParameter.lean 1 declarations
CrosscapEndpointSmoothArc.lean 1 declarations
CrosscapFiberIsolation.lean 3 declarations
CrosscapFormalPair.lean 1 declarations
CrosscapFrameHomotopy.lean 5 declarations
CrosscapFramedRectangle.lean 1 declarations
CrosscapGeometricCancellation.lean 1 declarations
CrosscapGermRestriction.lean 1 declarations
CrosscapHalfLineChart.lean 1 declarations
CrosscapJetStability.lean 1 declarations
CrosscapKernelCapture.lean 5 declarations
CrosscapKernelLine.lean 5 declarations
CrosscapLinearCoordinates.lean 8 declarations
CrosscapLinearStability.lean 3 declarations
CrosscapNormalDefect.lean 1 declarations
CrosscapNormalizedRectangle.lean 1 declarations
CrosscapOrderedArc.lean 1 declarations
CrosscapPairCoordinates.lean 1 declarations
CrosscapPairModel.lean 9 declarations
CrosscapPathInterior.lean 1 declarations
CrosscapRegularLocus.lean 1 declarations
CrosscapSecondDerivative.lean 3 declarations
CrosscapSourceEmbeddedPath.lean 1 declarations
CrosscapSourceEndpoint.lean 1 declarations
CrosscapStripFrame.lean 5 declarations
CrosscapStripRegularNeighborhood.lean 1 declarations
CurveBoundaryEmbeddedArc.lean 1 declarations
DoubleArcChartPartition.lean 2 declarations
DoubleArcExceptionalTimes.lean 2 declarations
DoubleChartReparametrization.lean 1 declarations
DoubleCurveBoundaryArc.lean 1 declarations
DoubleCurveBoundaryPaths.lean 1 declarations
DoubleCurveMembership.lean 2 declarations
DoubleCurveParameter.lean 1 declarations
DoubleCurveVelocities.lean 3 declarations
DoubleImageCoordinates.lean 1 declarations
DoubleLocusArc.lean 1 declarations
DoubleLocusAugmentation.lean 1 declarations
DoubleLocusChart.lean 1 declarations
DoubleLocusImmersion.lean 1 declarations
DoubleLocusProjections.lean 1 declarations
DoubleLocusSmoothStructure.lean 4 declarations
DoubleRotationFilling.lean 6 declarations
EmbeddedAxisCollar.lean 1 declarations
EndpointRegularArcs.lean 3 declarations
EndpointSignModel.lean 10 declarations
EqualIndexFrameFilling.lean 4 declarations
EuclideanImmersionReduction.lean 5 declarations
ExactCollarInterpolation.lean 9 declarations
ExactCollarRemainderBounds.lean 3 declarations
ExactRegularCollar.lean 1 declarations
FiniteArcPieces.lean 1 declarations
FiniteCleanPairRegularization.lean 1 declarations
FiniteCornerBridges.lean 1 declarations
FiniteCornerWindows.lean 1 declarations
FiniteCrosscapCancellation.lean 3 declarations
FiniteCrosscapCleanup.lean 2 declarations
FiniteCurveArcCover.lean 1 declarations
FiniteDoubleCurvePieces.lean 1 declarations
FiniteExceptionalDoublePairs.lean 1 declarations
FinitePairC1Regularization.lean 1 declarations
FinitePairPointRegularization.lean 1 declarations
FinitePairProtectedRegularization.lean 1 declarations
FiniteQuadraticCrosscaps.lean 1 declarations
FiniteRegularPathCover.lean 1 declarations
FiniteRegularPathSmooth.lean 2 declarations
FiniteSingularProjection.lean 5 declarations
FiniteSurfacePairRegularization.lean 1 declarations
FixedPairPointAvoidance.lean 1 declarations
FixedSurfacePairPatch.lean 3 declarations
FramedCrosscapDefect.lean 1 declarations
FramedCurveTube.lean 5 declarations
GeometricBoundaryCollar.lean 1 declarations
GlobalCleanPairRegularization.lean 1 declarations
GlobalPairRegularization.lean 1 declarations
GraphJoinArc.lean 5 declarations
HalfLineCompactArc.lean 2 declarations
HomotopyCollarDerivative.lean 5 declarations
InteriorRulingSupport.lean 1 declarations
LocalCornerBridge.lean 4 declarations
LocalCornerBridgeSeparation.lean 2 declarations
LocalDoubleCurveLift.lean 1 declarations
LoopDensityArcTriangle.lean 5 declarations
NarrowedRulingBounds.lean 2 declarations
NarrowedRulingJets.lean 3 declarations
NondegenerateCrosscapDefect.lean 1 declarations
NormalBoundaryCollar.lean 1 declarations
NormalCollarGluing.lean 2 declarations
NormalLinearizationHomotopy.lean 8 declarations
NormalizedFramedAxis.lean 1 declarations
NormalizedPairFilling.lean 1 declarations
OpenDoubleArcLift.lean 1 declarations
OppositeIndexFrameFilling.lean 4 declarations
OrderedArcEndpointUnique.lean 2 declarations
OrderedArcSeparation.lean 1 declarations
OrderedCornerBridges.lean 2 declarations
OrientedArcJoin.lean 1 declarations
OrientedChartArc.lean 1 declarations
OrientedDoubleChartArc.lean 1 declarations
OrientedDoubleTransition.lean 2 declarations
PairArcJoin.lean 2 declarations
PathCornerNeighborhood.lean 2 declarations
PerturbedCollarJets.lean 1 declarations
PreparedCrosscapNeighborhoods.lean 1 declarations
PreparedCrosscapSourcePath.lean 1 declarations
PreparedDoubleCurve.lean 1 declarations
PreparedSmoothCrosscapArc.lean 1 declarations
PrimitiveBoundaryCollar.lean 2 declarations
ProjectionCrosscapJet.lean 3 declarations
QuadraticCrosscapFactorization.lean 6 declarations
QuadraticCrosscapIsolation.lean 4 declarations
QuadraticCrosscapNormalForm.lean 1 declarations
QuadraticCrosscapPreparation.lean 1 declarations
QuadraticDoublePoints.lean 4 declarations
QuadraticDoubleTransverse.lean 5 declarations
RegularArcPaths.lean 6 declarations
RegularCrosscapRepresentatives.lean 1 declarations
RegularDoubleLocusImmersion.lean 1 declarations
RegularDoublePointNormalForm.lean 1 declarations
RegularHomotopyCollar.lean 1 declarations
RegularInteriorDoubleArc.lean 1 declarations
RegularPairedArcProjection.lean 1 declarations
RegularPathCornerChart.lean 2 declarations
RegularPathCornerPieces.lean 3 declarations
RegularPathCover.lean 5 declarations
RegularPathCoverConcat.lean 1 declarations
RegularPathCoverGerms.lean 2 declarations
RegularPathEndpointPieces.lean 4 declarations
RegularSheetDoubleChart.lean 1 declarations
RelativeFramePatching.lean 1 declarations
RelativeImmersionHPrinciple.lean 6 declarations
ReturningCornerArc.lean 1 declarations
ReturningCornerParameters.lean 3 declarations
RoundedReturnArc.lean 1 declarations
RuledCrosscapStrip.lean 2 declarations
RulingDirectionJet.lean 3 declarations
RulingHomotopy.lean 8 declarations
RulingLinearTarget.lean 2 declarations
RulingRemainder.lean 5 declarations
SameSideCollarHomotopy.lean 3 declarations
ScalarCollarData.lean 1 declarations
ScaledCrosscapCancellation.lean 4 declarations
SeparatedCornerBridge.lean 3 declarations
SharedParameterArcJoin.lean 1 declarations
ShiftedCollarDensity.lean 2 declarations
ShiftedRotationFilling.lean 7 declarations
ShiftedRotationFrame.lean 6 declarations
SignedCrosscapAxis.lean 1 declarations
SimpleCrosscapArc.lean 1 declarations
SimplePreparedCrosscaps.lean 1 declarations
SlowCollarCutoff.lean 1 declarations
SmallCollarAngle.lean 3 declarations
SmoothArcChartTransport.lean 1 declarations
SmoothArcJoin.lean 7 declarations
SmoothArcParameterExtension.lean 1 declarations
SmoothArcReverse.lean 1 declarations
SmoothArcStartGerm.lean 1 declarations
SmoothArcTail.lean 2 declarations
SmoothArcTimeDerivative.lean 1 declarations
SmoothCompactArc.lean 3 declarations
SmoothCrosscapAxisTangent.lean 1 declarations
SmoothCrosscapConnectingArc.lean 2 declarations
SmoothCrosscapSourceArc.lean 1 declarations
SmoothCrosscapSourceGeometry.lean 1 declarations
SmoothDoubleArc.lean 2 declarations
SmoothDoubleArcAppend.lean 1 declarations
SmoothDoubleArcExtension.lean 1 declarations
SmoothDoubleArcParameterization.lean 1 declarations
SmoothDoubleArcProjections.lean 1 declarations
SmoothDoubleAtlas.lean 6 declarations
SmoothDoubleTransitions.lean 4 declarations
SmoothFiniteRegularPath.lean 1 declarations
SmoothInteriorDoubleArc.lean 1 declarations
SmoothOrderedArc.lean 2 declarations
SmoothRegularZeroArc.lean 2 declarations
SmoothRelativeFrame.lean 2 declarations
SmoothSurfaceDoubleArc.lean 1 declarations
SmoothSurfaceDoubleChart.lean 2 declarations
SourceArcChart.lean 1 declarations
SourceMapRepresentative.lean 2 declarations
StandardCrosscapDerivative.lean 4 declarations
StandardPreparedCrosscaps.lean 2 declarations
SupportedCrosscapCancellation.lean 1 declarations
SupportedExactCollar.lean 1 declarations
SupportedFormalImmersion.lean 1 declarations
SupportedRuledInterior.lean 1 declarations
SurfaceArcTimeCoordinates.lean 1 declarations
SurfaceBoundaryCollar.lean 3 declarations
SurfaceCrosscapNormalForm.lean 1 declarations
SurfaceCrosscapPreparation.lean 1 declarations
SurfaceCrosscapTransverseNeighborhood.lean 1 declarations
SurfaceDoublePairChart.lean 1 declarations
SurfaceExactCollar.lean 1 declarations
SurfaceFormalImmersion.lean 1 declarations
SurfacePairDerivative.lean 3 declarations
SurfacePairLocalRegularization.lean 1 declarations
SurfacePairPatchTranslation.lean 1 declarations
SurfacePairPointAvoidance.lean 1 declarations
SurfaceQuadraticDoubleChart.lean 1 declarations
SurfaceRuledInterior.lean 1 declarations
TransversePreparedCrosscaps.lean 1 declarations
TransverseRuledSurface.lean 11 declarations
TwistedRuledCoordinates.lean 8 declarations
UnitIntervalArcImages.lean 2 declarations
UnorderedDoubleCurveChart.lean 1 declarations
UnorderedSurfacePairs.lean 11 declarations
VaryingFramedCurveTube.lean 6 declarations
WhitneyStartingGeometry.lean 2 declarations
WhitneySurfaceImmersion.lean 1 declarations
ZeroAmplitudeCollar.lean 1 declarations