Mankiewicz Extension Theorem

This owner-approved Project overview is derived from 11 canonical LFH Cards in the pinned MathlibAnnex Catalog. The exact source and Card bindings retain their existing clean-build, declaration-accounting, compiled-axiom, and source-exposition review evidence. This does not claim a line-by-line human audit of every Lean proof script or an independent reproof. The effective Exact Mathematics content terms apply to this presentation.

The goal

An isometry equivalence from an 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.

Why it matters

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 an 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 canonical statements.

Scope limits

This Project overview references exact canonical Cards and does not imply new formal qualification or a line-by-line human proof audit. Boundary Inputs include Lean Core, Mathlib, and omitted MathlibAnnex support declarations.