Declaration Card Catalog

The current whole-library Catalog contains 11 canonical Cards, all referenced by the Mankiewicz Project. Read the common verification contract

1. Mankiewicz extension on open connected domains

   MathlibAnnex.IsometryEquiv.existsUnique_affineExtension

2. Affine extension from open balls

   MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_ball

3. Affine extension from equal-radius closed balls

   MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_closedBall

4. Convex-set extension via ambient interiors

   MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex

5. Local affine-isometry chart on a smaller ball

   MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball

6. Center transport under bounded point-reflection symmetry

   MathlibAnnex.IsometryEquiv.map_center_of_reflectionInvariant

7. Affine-segment preservation on a quarter ball

   MathlibAnnex.IsometryEquiv.map_lineMap_of_mem_ball

8. Midpoint preservation on a quarter ball

   MathlibAnnex.IsometryEquiv.map_midpoint_of_mem_ball

9. Midpoint preservation on a symmetric lens

   MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens

10. Midpoint preservation under lens containment

    MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset

11. Symmetric lens

    MathlibAnnex.symmetricLens