OAI/Geometry/WeakMTW/Coordinates/
166 declarations, 0 contain sorry, 0 declared as axioms; 42 files
Files
- ChartGlobalVariation.lean 4 declarations
- ChartLength.lean 3 declarations
- ChartMetric.lean 7 declarations
- ChartPairing.lean 3 declarations
- ChartScaling.lean 2 declarations
- CoerciveMetric.lean 2 declarations
- CoordinateEquation.lean 2 declarations
- CoordinateExistence.lean 1 declarations
- CoordinateGeometry.lean 19 declarations
- CoordinateIdentification.lean 1 declarations
- CoordinateLocal.lean 3 declarations
- CostEndpointAction.lean 3 declarations
- CostFirstTaylor.lean 1 declarations
- CostNormalGradient.lean 2 declarations
- EndpointAction.lean 5 declarations
- FanCoordinates.lean 10 declarations
- FocalCoordinates.lean 6 declarations
- InteriorCost.lean 4 declarations
- IntrinsicNormal.lean 1 declarations
- LocalCost.lean 3 declarations
- LocalDistance.lean 8 declarations
- NormalAction.lean 4 declarations
- NormalCoordinates.lean 3 declarations
- NormalCurve.lean 1 declarations
- NormalDifferential.lean 5 declarations
- NormalEndpoint.lean 3 declarations
- NormalFlowLength.lean 4 declarations
- NormalLength.lean 3 declarations
- NormalMetricSpeed.lean 3 declarations
- NormalNeighborhood.lean 4 declarations
- NormalRigidity.lean 2 declarations
- NormalState.lean 2 declarations
- PairExpCoordinates.lean 7 declarations
- PairNormalDistance.lean 3 declarations
- RadialCoordinates.lean 9 declarations
- RadialLength.lean 6 declarations
- RadialRigidity.lean 3 declarations
- TangentCoordinates.lean 6 declarations
- TangentDiskCompact.lean 2 declarations
- TangentScaling.lean 3 declarations
- TwoPointSpeed.lean 2 declarations
- UnitNormal.lean 1 declarations