MATHLIBANNEX / CANONICAL DECLARATION CARD

Affine-segment preservation on a quarter ball

MathlibAnnex.IsometryEquiv.map_lineMap_of_mem_ball

theorem

Passes from midpoint preservation to every real parameter in a segment.

Statement

Let be real normed spaces, a bijective isometry between subsets, and . Assume , and . For and ,

Assumptions

Both radius- open balls are contained in their respective sets. Both endpoints lie in the source quarter ball. The parameter is restricted to .

Conclusion

The same isometry preserves every point of the segment between these endpoints, with the same parameter .

Proof route

On the convex quarter ball, midpoint preservation gives an arithmetic progression at rational subdivision points. Continuity then gives all real parameters in the interval.

Proof steps

  1. Put . If and , then

    Hence . Restrict to . By Quarter-ball midpoint theorem, for all .

  2. Fix and set

    Step 1 puts every in . Since , midpoint preservation gives

    Thus the successive differences are constant.

  3. Summing the constant differences and using , gives

    This proves the desired formula for every rational parameter in .

  4. For real , choose rationals . The isometry is continuous, and

    The affine combination on the right is continuous as well, so the rational identity passes to the limit. Replacing by the restriction of proves the theorem.

Main citations

Lean source signature (exact)

theorem map_lineMap_of_mem_ball
    {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) {R : ℝ} (hR : 0 < R)
    (hsball : ball (c : E) R ⊆ s)
    (htball : ball ((f c : t) : F) R ⊆ t)
    (x y : s) (hx : (x : E) ∈ ball (c : E) (R / 4))
    (hy : (y : E) ∈ ball (c : E) (R / 4))
    (a : ℝ) (ha : a ∈ Icc (0 : ℝ) 1) :
    ((f ⟨AffineMap.lineMap (x : E) (y : E) a,
          hsball (ball_subset_ball (by linarith : R / 4 ≤ R)
            ((convex_ball (c : E) (R / 4)).lineMap_mem hx hy ha))⟩ : t) : F) =
      AffineMap.lineMap ((f x : t) : F) ((f y : t) : F) a
In the source Mathematical meaning
(f : s ≃ᵢ t) (c : s) The distance-preserving bijection and center , with in real normed spaces.
{R : ℝ} (hR : 0 < R) The common radius .
(hsball : ball (c : E) R ⊆ s) The open ball lies in the source set.
(htball : ball ((f c : t) : F) R ⊆ t) The open ball lies in the target set; this is a separate hypothesis.
(x y : s) Two points .
(hx : (x : E) ∈ ball (c : E) (R / 4)) The inequality .
(hy : (y : E) ∈ ball (c : E) (R / 4)) The inequality for the other point.
(a : ℝ) (ha : a ∈ Icc (0 : ℝ) 1) A real coefficient with .
AffineMap.lineMap (x : E) (y : E) a The point of .
(convex_ball (c : E) (R / 4)).lineMap_mem hx hy ha The derived membership of that point in the quarter ball, using convexity, both endpoint bounds and .
hsball (ball_subset_ball The subsequent inclusion into and then , which makes a valid application.
AffineMap.lineMap ((f x : t) : F) ((f y : t) : F) a The output expression ; the whole conclusion equates it with the image of the source segment point.

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.IsometryEquiv.map_lineMap_of_mem_ball

Accepted content SHA-256: d615f4324cf6c19ea0b4850824feec7c1afce45a9859e5a7809367e9a78ca67f

Accepted source guide SHA-256: 5e52d4375dbd277c1b17fc4a7d1b7119053d67200a81615ab306c3335b7e8535

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑