OAI/Geometry/IsometricImmersion/Main.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Geometry.coordinateSquareOpen line 12

   Also declared: ComparatorChallenges/IsometricImmersion.lean:43 (same declaration text).

2. theorem OAI.SmoothLocal.Geometry.zero_mem_coordinateSquareOpen line 15
3. theorem OAI.SmoothLocal.Geometry.relativelyOpen_square_iff line 19
4. theorem OAI.SmoothLocal.Geometry.counterexampleMetric_local_smoothPositive line 36
5. theorem OAI.SmoothLocal.Geometry.counterexampleMetric_no_subtype_isometric_immersion line 41
6. theorem OAI.SmoothLocal.Geometry.exists_local_metric_without_local_immersion line 49

   Distinct definitions of this name: ComparatorChallenges/IsometricImmersion.lean:46 (same statement text; different proof or body). Qualify references as OAI.SmoothLocal.Geometry.exists_local_metric_without_local_immersion@path.