OAI/Geometry/Immersion/ClosedSurface/MetricModel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClosedSurfaceR4.Plane line 11

   Also declared: ComparatorChallenges/SurfaceImmersion.lean:11 (same declaration text).

2. abbrev OAI.ClosedSurfaceR4.Space line 12

   Also declared: ComparatorChallenges/SurfaceImmersion.lean:12 (same declaration text).

3. abbrev OAI.ClosedSurfaceR4.planeModel line 13

   Also declared: ComparatorChallenges/SurfaceImmersion.lean:13 (same declaration text).

4. abbrev OAI.ClosedSurfaceR4.spaceModel line 14

   Distinct definitions of this name: ComparatorChallenges/SurfaceImmersion.lean:14 (same statement text; different proof or body). Qualify references as OAI.ClosedSurfaceR4.spaceModel@path.

5. abbrev OAI.ClosedSurfaceR4.SmoothMetric line 21

   Also declared: ComparatorChallenges/SurfaceImmersion.lean:22 (same declaration text).

6. def OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion line 27

   Also declared: ComparatorChallenges/SurfaceImmersion.lean:26 (same declaration text).