Mankiewicz Extension Theorem

MathlibAnnex.IsometryEquiv.map_center_of_reflectionInvariant

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.

Exact source

MathlibAnnex.symmetricLens

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

Exact source

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens

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

Exact source

MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset

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

Exact source

MathlibAnnex.IsometryEquiv.map_midpoint_of_mem_ball

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

Exact source

MathlibAnnex.IsometryEquiv.map_lineMap_of_mem_ball

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

Exact source

MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball

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

Exact source

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension

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.

Exact source

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_ball

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.

Exact source

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex

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.

Exact source

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_closedBall

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.

Exact source