MATHLIBANNEX / CANONICAL DECLARATION CARD

Midpoint preservation on a quarter ball

MathlibAnnex.IsometryEquiv.map_midpoint_of_mem_ball

theorem

Supplies both lens inclusions from matching ambient balls.

Statement

Let be real normed spaces, , , and a bijective isometry. Let and satisfy and , where . For ,

Assumptions

Both ambient open-ball inclusions, positivity of , and membership of both in the quarter ball are required. The sets need not themselves be open or convex.

Conclusion

The midpoint belongs to , and the same isometry preserves that midpoint.

Proof route

Use radius for the source and target lenses. The quarter-ball bounds leave enough room for both lenses inside the given radius- balls.

Proof steps

  1. The triangle inequality gives , so . Also

    Thus the midpoint is a valid argument of .

  2. For ,

    Hence this entire lens lies in .

  3. Isometry gives . If , then

    The target ball assumption now puts the entire target lens in .

  4. Apply Midpoint preservation under two lens inclusions to this , the points , and the radius . Step 1 supplies its half-distance bound, and Steps 2–3 supply its two inclusions. Its output is exactly the claimed midpoint equation.

Main citations

Lean source signature (exact)

theorem map_midpoint_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)) :
    ((f ⟨midpoint ℝ (x : E) (y : E),
          hsball (by
            rw [mem_ball]
            calc
              dist (midpoint ℝ (x : E) (y : E)) (c : E) ≤
                  (dist (x : E) (c : E) + dist (y : E) (c : E)) / 2 := by
                    simpa [dist_comm] using
                      dist_midpoint_midpoint_le (x : E) (y : E) (c : E) (c : E)
              _ < R := by rw [mem_ball] at hx hy; linarith)⟩ : t) : F) =
      midpoint ℝ ((f x : t) : F) ((f y : t) : F)
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.
hsball (by The following proof block verifies that from the displayed distance estimate. It is not an extra assumption.
midpoint ℝ ((f x : t) : F) ((f y : t) : F) The right side is . The entire equality says that applying to the source midpoint gives this point in .

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_midpoint_of_mem_ball

Accepted content SHA-256: e19ce25a3ad10fdfca363466e027beec33a87addbaa5acb304642b4fe1ed3caf

Accepted source guide SHA-256: bfc080efac19e4c51ee91abba08bb204ed986f22a088cd8eef3c8d572fa2d97c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑