IndisputableMonolith.Foundation.CircleParam

declarations in this module (17)

• abbrev SphereOneAmbient L28
• abbrev SphereOneCarrier L32
• def sphereOneBaseVector L36
• theorem sphereOneBaseVector_mem_sphere L40
• def sphereOneBasepoint L46
• def trigCircleVector L50
• theorem trigCircleVector_mem_sphere L55
• theorem continuous_trigCircleVector L66
• def trigCirclePoint L78
• theorem continuous_trigCirclePoint L83
• theorem trigCirclePoint_zero L89
• theorem trigCirclePoint_two_pi L99
• def constantSphereOneSingularOneSimplex L109
• def constantSphereOneSingularZeroSimplex L115
• theorem constantSphereOneSingularOneSimplex_face_zero L122
• theorem constantSphereOneSingularOneSimplex_face_one L130
• theorem constantSphereOneSingularOneSimplex_faces_eq L137