OAI/Geometry/SplitTangent/
1950 declarations, 0 contain sorry, 0 declared as axioms; 110 files
Files
- ActualQuotientCharts.lean 15 declarations
- AllCompactLeaves.lean 4 declarations
- AllProjectiveLeaves.lean 7 declarations
- AmbientLeafGerm.lean 2 declarations
- AmbientLeafSectionBound.lean 2 declarations
- AmbientLeafSections.lean 9 declarations
- AnalyticFiniteRelations.lean 5 declarations
- ArbitraryPlaqueLeaves.lean 4 declarations
- Basic.lean 22 declarations
- BasicDerivativeKernel.lean 6 declarations
- BasicSubmersionTransport.lean 5 declarations
- BoxFirstTransport.lean 18 declarations
- BoxMonomials.lean 10 declarations
- BoxRelationLocus.lean 8 declarations
- BoxTransportBase.lean 28 declarations
- BracketIntegrability.lean 64 declarations
- ChartSubmersion.lean 1 declarations
- CompactLeafQuotient.lean 16 declarations
- CompactPolynomialRelations.lean 3 declarations
- CompactPositiveLeaf.lean 4 declarations
- CompactSetLimits.lean 5 declarations
- ComplementaryLeafIntersections.lean 3 declarations
- CoveringProductBackend.lean 3 declarations
- CurveHomogeneousSections.lean 6 declarations
- DenseCompactLeaves.lean 4 declarations
- DenseRationalVariation.lean 2 declarations
- EmbeddedHolomorphicAtlas.lean 10 declarations
- EmbeddedLeafCharts.lean 14 declarations
- EmbeddedPlaqueChart.lean 10 declarations
- EmbeddedRationalCurve.lean 3 declarations
- EmbeddedTangentLift.lean 9 declarations
- EverywhereSmoothLeafQuotient.lean 2 declarations
- FamilyPropagationStep.lean 25 declarations
- FiniteOpenMaps.lean 6 declarations
- FoliationLeaves.lean 14 declarations
- FormalBoxes.lean 706 declarations
- GenericFiniteCovering.lean 5 declarations
- GenericLeafProductCover.lean 6 declarations
- GlobalAffineRelations.lean 1 declarations
- GlobalLeafRelations.lean 3 declarations
- GlobalProducts.lean 2 declarations
- GlobalTensorVanishing.lean 3 declarations
- GlobalTopologicalProduct.lean 8 declarations
- HolomorphicBasicTransport.lean 6 declarations
- HolomorphicCommonZeros.lean 4 declarations
- HolomorphicHypersurfaces.lean 5 declarations
- HolomorphicLeafBasic.lean 3 declarations
- HolomorphicLocalDiffeomorph.lean 6 declarations
- HolomorphicManifoldProduct.lean 7 declarations
- HolomorphicTangentMapAt.lean 1 declarations
- IntegrabilityReduction.lean 5 declarations
- IntrinsicPositiveLeaf.lean 1 declarations
- LeadingJetProduct.lean 2 declarations
- LeafAffineRelations.lean 1 declarations
- LeafAlgebraicDependence.lean 3 declarations
- LeafClosureRelations.lean 3 declarations
- LeafCompactLimits.lean 5 declarations
- LeafGermIdentity.lean 3 declarations
- LeafHomogeneousRelations.lean 1 declarations
- LeafJetAtlas.lean 12 declarations
- LeafLimitRelations.lean 2 declarations
- LeafLimitsSinglePlaque.lean 3 declarations
- LeafPlaques.lean 9 declarations
- LeafPolynomialGrowth.lean 8 declarations
- LeafProducts.lean 4 declarations
- LeafRank.lean 5 declarations
- LeafTopology.lean 4 declarations
- ManifoldJetAnalytic.lean 3 declarations
- ManifoldLeafJets.lean 12 declarations
- OpenManifold.lean 9 declarations
- OpenPositiveLeaves.lean 6 declarations
- PlaqueConnectedSets.lean 2 declarations
- PlaqueTangentImage.lean 1 declarations
- PolynomialLeafGerms.lean 5 declarations
- PolynomialRelationLocus.lean 5 declarations
- PolynomialSpecialization.lean 5 declarations
- PositiveCoverLift.lean 8 declarations
- PositiveJetFiltration.lean 4 declarations
- PositiveTangentCurves.lean 6 declarations
- ProductCriteria.lean 3 declarations
- ProjectiveHypersurfaces.lean 8 declarations
- ProjectiveLineFrame.lean 6 declarations
- ProjectiveLinearCoordinates.lean 7 declarations
- ProjectivePositiveLeaf.lean 4 declarations
- ProjectiveTangentBox.lean 3 declarations
- QuotientSubmersions.lean 4 declarations
- RCCovariantVanishing.lean 10 declarations
- RationalAccepted.lean 3 declarations
- RationalCoverLift.lean 3 declarations
- RationalCurveFrames.lean 17 declarations
- RationalEncoding.lean 4 declarations
- RationalFamilies.lean 59 declarations
- RationalFamilyCover.lean 2 declarations
- RationalReparam.lean 7 declarations
- RationalTrivialization.lean 217 declarations
- RationalVariation.lean 5 declarations
- SmoothLeafManifold.lean 12 declarations
- SmoothLeafProjection.lean 10 declarations
- SmoothLeafQuotient.lean 12 declarations
- SwappedProductChart.lean 5 declarations
- SymmetricConormalBound.lean 4 declarations
- TangentCurveLeaf.lean 4 declarations
- TangentRationalChains.lean 14 declarations
- TensorSectionSpace.lean 8 declarations
- TensorSpanning.lean 2 declarations
- TensorVanishing.lean 244 declarations
- TransverseDiscrete.lean 3 declarations
- TransverseQuotient.lean 7 declarations
- TwistedCurveTensor.lean 8 declarations
- ZariskiPairOpen.lean 3 declarations