OAI/Geometry/CylinderCovering/Convexity/
420 declarations, 0 contain sorry, 0 declared as axioms; 72 files
Files
- AffineSimplexChord.lean 10 declarations
- AmbientCylinderBridge.lean 5 declarations
- AmbientCylinderDefinitions.lean 1 declarations
- CanonicalRegularSimilarity.lean 1 declarations
- CompactC1Remainder.lean 2 declarations
- CompactEigenframes.lean 3 declarations
- CompactOuterConvergence.lean 4 declarations
- CompactParallelogramApproximation.lean 5 declarations
- CompactParallelogramCover.lean 2 declarations
- CompactProductEigenframes.lean 3 declarations
- CompactSpectralBounds.lean 1 declarations
- ConvexBodyShadowBounds.lean 11 declarations
- ConvexOpenEnlargement.lean 2 declarations
- ConvexPerturbationInverse.lean 3 declarations
- CylinderBridge.lean 10 declarations
- CylinderBridgeDefinitions.lean 1 declarations
- CylinderSimilarity.lean 21 declarations
- EigenframeBounds.lean 7 declarations
- FiniteCauchyVariation.lean 7 declarations
- FiniteLatticeNeighborhood.lean 6 declarations
- FinitePlaneHausdorff.lean 5 declarations
- FinitePlaneMeasure.lean 1 declarations
- GeneralCapArea.lean 16 declarations
- GeneralCapAreaDefinitions.lean 4 declarations
- GeneralCapCoverage.lean 15 declarations
- GeneralCapFamily.lean 7 declarations
- GeneralCapScalarHelpers.lean 8 declarations
- GlobalDefinitions.lean 11 declarations
- InverseSqrtBounds.lean 3 declarations
- IsometricCylinderEmbedding.lean 29 declarations
- IsometricCylinderEmbeddingDefinitions.lean 6 declarations
- LevelCrossing.lean 6 declarations
- NormalFrame.lean 20 declarations
- NormalFrameDefinitions.lean 7 declarations
- NormalFrameProjection.lean 3 declarations
- OpenBaseApproximation.lean 4 declarations
- OpenBaseApproximationDefinitions.lean 3 declarations
- OpenBaseComparison.lean 3 declarations
- OpenBaseThickening.lean 4 declarations
- OpenParallelogram.lean 6 declarations
- OpenParallelogramComparison.lean 1 declarations
- OpenParallelogramDefinitions.lean 4 declarations
- OpenThickening.lean 1 declarations
- OrthonormalHeightComparison.lean 9 declarations
- OrthonormalHeightComparisonDefinitions.lean 8 declarations
- PairedFamilyDefinitions.lean 1 declarations
- ParallelogramGeometry.lean 8 declarations
- ProjectionShapeSupport.lean 4 imports, no declarations
- QuadraticTaylorBound.lean 5 declarations
- RegularAngularDefinitions.lean 1 declarations
- RegularBaseVariants.lean 4 declarations
- RegularCounterexamples.lean 3 declarations
- RegularOpenParallelogram.lean 2 declarations
- RegularSimilarityBasis.lean 4 declarations
- RegularSimplexSimilarity.lean 6 declarations
- RelativeCostComparison.lean 6 declarations
- RelaxedInversion.lean 1 declarations
- ResidualDisk.lean 9 declarations
- SimilarityDefinitions.lean 9 declarations
- SlidingRowCertificates.lean 2 declarations
- SpectralNormComparison.lean 19 declarations
- SpectralNormComparisonDefinitions.lean 4 declarations
- SquaredCapCover.lean 7 declarations
- SquaredCapCoverDefinitions.lean 2 declarations
- SquaredCapData.lean 1 declarations
- SquaredCapDataDefinitions.lean 1 declarations
- TetrahedronIdentification.lean 3 declarations
- ThresholdInverse.lean 7 declarations
- ThresholdInversion.lean 10 declarations
- ThresholdRemainder.lean 4 declarations
- TriangularSimilarity.lean 7 declarations
- UniformTaylor.lean 5 declarations