MATHLIBANNEX / PROJECT LFH

Mankiewicz Extension Theorem

MathlibAnnex / Theorem Project

The mathematical 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.

Exact source: MathlibAnnex v0.4.0 Project entry · Source manifest

Eleven reviewed canonical Declaration Cards remain independent records. Project relations navigate within this page.

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 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.

Proof architecture

Reflection to midpoint rigidity

A bounded symmetric lens is reflection-invariant about the midpoint. Center rigidity sends that midpoint to the target midpoint, first on lenses and then on contained balls.

Local affinity through omitted support lemmas

Midpoint preservation yields line-map preservation. Radial-map support declarations, including private technical lemmas, connect this result to a local affine isometric extension. The path witnesses retain these declarations even though they are outside the selected Card scope.

Global assembly and specializations

Local extensions agree and assemble over an open connected domain. A convex source with nonempty ambient interior, together with exact preservation of ambient-interior membership, yields the convex specialization; open- and closed-ball corollaries follow under their exact radius conditions. The closed-ball route also uses reflection rigidity.

Boundary Inputs

961 exact Boundary Inputs: EXTERNAL_COMPILED_DECLARATION 896, OMITTED_INTERNAL_NATIVE_DECLARATION 65. Selected reachability is retained through every omitted internal declaration.

Inspect Boundary Inputs
  • NormedAddCommGroup — Compiled external provider used by selected Project declarations.
  • NormedAddCommGroup.toSeminormedAddCommGroup — Compiled external provider used by selected Project declarations.
  • Real — Compiled external provider used by selected Project declarations.
  • Set — Compiled external provider used by selected Project declarations.
  • AddCommGroup.toDivisionAddCommMonoid — Compiled external provider used by selected Project declarations.
  • AddCommMonoidWithOne.toAddMonoidWithOne — Compiled external provider used by selected Project declarations.
  • AddGroup.toSubNegMonoid — Compiled external provider used by selected Project declarations.
  • AddGroupWithOne.toAddGroup — Compiled external provider used by selected Project declarations.
  • AddGroupWithOne.toAddMonoidWithOne — Compiled external provider used by selected Project declarations.
  • AddMonoid.toAddSemigroup — Compiled external provider used by selected Project declarations.
  • AddMonoidWithOne — Compiled external provider used by selected Project declarations.
  • AddMonoidWithOne.toNatCast — Compiled external provider used by selected Project declarations.
  • AddMonoidWithOne.toOne — Compiled external provider used by selected Project declarations.
  • AddSemigroup.toAdd — Compiled external provider used by selected Project declarations.
  • AffineIsometryEquiv — Compiled external provider used by selected Project declarations.

Dependency-first reading route

Levels belong to this Project. Select a level or follow a relation to another declaration tile.

11 declarations

Level 0

2 declarations
Level 0Theorem ProjectFocus target

Center transport under bounded point-reflection symmetry

MathlibAnnex.IsometryEquiv.map_center_of_mapsTo_pointReflection

f maps the source reflection center to the target reflection center.

Statement in Project context

Let f:s≃ᵢt be an isometry equivalence between subsets of real normed affine spaces. Suppose c∈s and d∈t, the source set s is bounded, and s and t are invariant under point reflection about c and d respectively. Then f(c)=d as subtype points.

Immediate prerequisites in this Project
None in this Project

Used by in this Project
Midpoint preservation on a symmetric lens

Level 0Theorem ProjectFocus target

Symmetric lens

MathlibAnnex.symmetricLens

The symmetric lens is the intersection of the closed radius-r balls centered at x and y. This definition needs no positivity assumption.

Statement in Project context

`symmetricLens x y r` is the intersection of the two closed balls of radius r centered at x and y.

Immediate prerequisites in this Project
None in this Project

Used by in this Project
Midpoint preservation on a symmetric lens

Level 1

1 declaration
Level 1Theorem ProjectFocus target

Midpoint preservation on a symmetric lens

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens

The isometry maps the midpoint of the source foci to the midpoint of the target foci.

Statement in Project context

Assume the midpoint of x,y belongs to symmetricLens(x,y,r), and likewise the midpoint of x′,y′ belongs to symmetricLens(x′,y′,r), as expressed by the two half-distance inequalities. Any isometry equivalence between these lenses maps midpoint(x,y) to midpoint(x′,y′).

Level 2

1 declaration
Level 2Theorem ProjectFocus target

Midpoint preservation under lens containment

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset

f preserves the midpoint of x and y. The target half-distance bound follows from the isometry.

Statement in Project context

Let f:s≃ᵢt and x,y∈s. If the symmetric lens of radius r around x,y lies in s, the corresponding lens around f(x),f(y) lies in t, and half the distance between x and y is at most r, then f sends midpoint(x,y) to midpoint(f(x),f(y)).

Immediate prerequisites in this Project
Midpoint preservation on a symmetric lens

Used by in this Project
Midpoint preservation on a quarter ball

Level 3

1 declaration
Level 3Theorem ProjectFocus target

Midpoint preservation on a quarter ball

MathlibAnnex.IsometryEquiv.map_midpoint_of_mem_ball

f sends the midpoint of x and y to the midpoint of f(x) and f(y).

Statement in Project context

Let f:s≃ᵢt and let c∈s. Assume R>0, ball(c,R)⊆s, and ball(f(c),R)⊆t. If x,y∈s both lie in ball(c,R/4), then f sends their midpoint to the midpoint of f(x) and f(y).

Immediate prerequisites in this Project
Midpoint preservation under lens containment

Used by in this Project
Affine-segment preservation on a quarter ball

Level 4

1 declaration
Level 4Theorem ProjectFocus target

Affine-segment preservation on a quarter ball

MathlibAnnex.IsometryEquiv.map_lineMap_of_mem_ball

f preserves the affine combination (1-a)x + ay, with the exact subtype membership witnesses supplied in Lean.

Statement in Project context

Under the same ambient-ball hypotheses as the local midpoint theorem, if x and y lie in ball(c,R/4), then for every a in [0,1], f sends the affine point lineMap(x,y,a) to lineMap(f(x),f(y),a).

Immediate prerequisites in this Project
Midpoint preservation on a quarter ball

Used by in this Project
Local affine-isometry chart on a smaller ball

Level 5

1 declaration
Level 5Theorem ProjectFocus target

Local affine-isometry chart on a smaller ball

MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball

An ambient affine isometry equivalence agrees with f on the ball about c of radius R/8.

Statement in Project context

Suppose a set isometry f:s≃ᵢt is defined on subsets containing the ambient balls ball(c,R) and ball(f(c),R), with R>0. Then there is an ambient real affine isometry equivalence A that agrees with f at every source point lying in the smaller ball ball(c,R/8).

Immediate prerequisites in this Project
Affine-segment preservation on a quarter ball

Used by in this Project
Mankiewicz extension on open connected domains

Level 6

1 declaration
Level 6Theorem ProjectFocus target

Mankiewicz extension on open connected domains

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension

There is a unique ambient real affine isometry equivalence whose restriction to s is f.

Statement in Project context

Let f be a surjective isometry from an open connected subset s of a real normed space onto an open subset t of another real normed space. Then there exists a unique ambient real affine isometry equivalence A agreeing with f on all of s. Target connectedness is not a separate assumption.

Level 7

2 declarations
Level 7Theorem ProjectFocus target

Affine extension from open balls

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_ball

f extends uniquely to an ambient real affine isometry equivalence. The two positive radii need not be assumed equal.

Statement in Project context

Let f be a surjective isometry from the open ball ball(c,r) onto the open ball ball(d,R) in real normed spaces, where r>0 and R>0; the two radii need not be equal. Then there is a unique ambient real affine isometry equivalence A such that A(x)=f(x) for every x in the source ball.

Immediate prerequisites in this Project
Mankiewicz extension on open connected domains

Used by in this Project
None in this Project

Level 7Theorem ProjectFocus target

Convex-set extension via ambient interiors

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex

f extends uniquely to an ambient real affine isometry equivalence. No additional convexity assumption on t is stated.

Statement in Project context

Let f be a surjective isometry from a convex subset s of a real normed space onto a subset t. Assume the ambient interior of s is nonempty and, for every x in s, x lies in interior(s) if and only if f(x) lies in interior(t). Then f extends uniquely to an ambient real affine isometry equivalence. No separate convexity assumption on t is required by this statement.

Immediate prerequisites in this Project
Mankiewicz extension on open connected domains

Used by in this Project
Affine extension from equal-radius closed balls

Level 8

1 declaration
Level 8Theorem ProjectFocus target

Affine extension from equal-radius closed balls

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_closedBall

f extends uniquely to an ambient real affine isometry equivalence.

Statement in Project context

Let f be a surjective isometry between the closed balls closedBall(c,r) and closedBall(d,r) of the same radius r>0 in real normed spaces. Then f has a unique ambient real affine isometry-equivalence extension agreeing with f on the whole source closed ball.

Immediate prerequisites in this Project
Convex-set extension via ambient interiors

Used by in this Project
None in this Project