Historical full-source exploration. Declaration counts here are source declarations, not the selected Card count. Return to selected Card reading
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.
Symmetric lens · Center transport under bounded point-reflection symmetry · Midpoint preservation on a quarter ball
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.
Affine-segment preservation on a quarter ball · Local affine-isometry chart on a smaller ball
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.
Mankiewicz extension on open connected domains · Convex-set extension via ambient interiors · Affine extension from open balls · Affine extension from equal-radius closed balls
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.
Level 0
2 declarationsCenter 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
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 declarationMidpoint 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′).
Immediate prerequisites in this Project
Center transport under bounded point-reflection symmetry, Symmetric lens
Used by in this Project
Midpoint preservation under lens containment
Level 2
1 declarationMidpoint 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 declarationMidpoint 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 declarationAffine-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 declarationLocal 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 declarationMankiewicz 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.
Immediate prerequisites in this Project
Local affine-isometry chart on a smaller ball
Used by in this Project
Affine extension from open balls, Convex-set extension via ambient interiors
Level 7
2 declarationsAffine 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
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 declarationAffine 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