Mankiewicz Extension Theorem | Exact Mathematics

MathlibAnnex / Selected reading scope

The mathematical goal

An isometry equivalence from a nonempty open connected subset onto an open subset of real normed spaces extends uniquely to an affine isometry equivalence of the ambient spaces. The selected route also reaches convex-domain and ball specializations.

11 approved Cards in this selected reading scope. The catalog contains 188 distinct Cards across the four Projects.

Scope

Local distance information becomes a rigid affine structure. This Project exposes the reusable chain from reflection and midpoint geometry to global extension.

Hypotheses

Real normed spaces and an isometry equivalence. The principal theorem requires a nonempty open connected source and an open target. The convex specialization requires a convex source set with nonempty ambient interior and exact preservation of ambient-interior membership; the target set is not separately assumed convex. Exact assumptions, including radius conditions for balls, remain in the linked exact declarations.

Scope limits

The eleven declaration explanations are reviewed for source-exposition correspondence. This does not claim a line-by-line human proof audit. Boundary Inputs include Lean Core, Mathlib, and omitted MathlibAnnex support declarations.

Mathematical routes

Reflection symmetry identifies midpoints, and midpoint preservation yields local affine-isometry charts. Agreement on open overlaps glues these charts over the nonempty open connected domain. Convex and ball consequences keep their separate interior and radius hypotheses.

Each route shows its direct Cards and the reused prerequisites needed in the selected reading graph. Shared Cards count once within each route and once in the Catalog.

Reflection and midpoint rigidity

A bounded symmetric lens and reflection-center rigidity identify midpoints under an isometry. Containment in matching ambient balls supplies the local hypotheses for midpoint preservation.

5 direct Cards + 0 reused prerequisites = 5 unique Cards. Shared Cards count once in this route.

Key result: Midpoint preservation on a quarter ball
Key definition: Symmetric lens

Read this route with prerequisites

Local affine-isometry charts

Midpoint preservation yields preservation of affine segments on a smaller ball. The exact source path through omitted radial-map helpers constructs one ambient affine isometry agreeing with the given map there.

2 direct Cards + 5 reused prerequisites = 7 unique Cards. Shared Cards count once in this route.

Key result: Local affine-isometry chart on a smaller ball
Key result: Affine-segment preservation on a quarter ball

Read this route with prerequisites

Global extension and specializations

Local affine-isometry charts agree on open overlaps and glue over a nonempty open connected source. Continuity and interior matching yield the convex, open-ball and equal-radius closed-ball specializations with their stated hypotheses.

4 direct Cards + 7 reused prerequisites = 11 unique Cards. Shared Cards count once in this route.

Key result: Mankiewicz extension on open connected domains
Related specialization: Affine extension from equal-radius closed balls

Read this route with prerequisites

Dependency-first reading route

Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.