OAI/Analysis/SphereIsometry/
747 declarations, 0 contain sorry, 0 declared as axioms; 67 files
Files
- AlignedConfiguration.lean 39 declarations
- Alignment.lean 2 declarations
- AlignmentSet.lean 1 declarations
- BarycentricBasic.lean 11 declarations
- BarycentricFlags.lean 13 declarations
- BarycentricIncidence.lean 13 declarations
- BarycentricMesh.lean 5 declarations
- BarycentricPoints.lean 2 imports, no declarations
- BarycentricPurity.lean 4 declarations
- BarycentricRestriction.lean 13 declarations
- BarycentricSupport.lean 10 declarations
- BarycentricZero.lean 5 declarations
- Basic.lean 26 declarations
- ChordContradiction.lean 1 declarations
- ChordSecant.lean 19 declarations
- CoefficientBins.lean 4 declarations
- CompactApproximation.lean 17 declarations
- CompactConvexFixedPoint.lean 8 declarations
- CondensingFixedPoint.lean 2 declarations
- CondensingIteration.lean 23 declarations
- ConvexCoverRegroup.lean 3 declarations
- ConvexDiameter.lean 2 declarations
- DefectAttainment.lean 5 declarations
- DefectSequence.lean 3 declarations
- DiameterBounds.lean 4 declarations
- Extension.lean 14 declarations
- ExtremalPropagation.lean 20 declarations
- FiniteComplex.lean 25 declarations
- InvariantConvexSet.lean 17 declarations
- IteratedPoints.lean 13 declarations
- IteratedSubdivision.lean 6 imports, no declarations
- KuratowskiBasic.lean 17 declarations
- KuratowskiConvexHull.lean 4 declarations
- KuratowskiNested.lean 2 declarations
- KuratowskiTotalBounded.lean 3 declarations
- LargeChord.lean 5 declarations
- Main.lean 4 imports, no declarations
- Model.lean 2 declarations
- PositiveConvexFace.lean 18 declarations
- PositiveScheduling.lean 26 declarations
- ProbabilitySimplex.lean 13 declarations
- RadialContact.lean 18 declarations
- RadialExtension.lean 21 declarations
- RadialPerturbation.lean 4 declarations
- ReturnMap.lean 60 declarations
- ReturnMapBounds.lean 6 declarations
- ReturnMapEstimate.lean 6 declarations
- ReturnMapFixedPoint.lean 1 declarations
- ReturnMapNoncompactness.lean 2 declarations
- ScalarBins.lean 1 declarations
- SimplexFixedPoint.lean 2 declarations
- SimplexLimit.lean 4 declarations
- SmallChord.lean 4 declarations
- Sperner.lean 2 declarations
- SpernerBoundary.lean 15 declarations
- SpernerFacet.lean 9 declarations
- SpernerIncidence.lean 3 declarations
- SphereCompletion.lean 22 declarations
- SubdivisionData.lean 22 declarations
- SubdivisionIncidence.lean 3 declarations
- SubdivisionPointRestriction.lean 4 declarations
- SubdivisionRestriction.lean 13 declarations
- Supports.lean 19 declarations
- UltraNormed.lean 41 declarations
- UltraRealLimit.lean 26 declarations
- UltraSphere.lean 21 declarations
- UnitRepresentatives.lean 6 declarations