Exact UTF-8 source: MathlibAnnex/Analysis/Normed/Affine/IsometryExtension/Ball.lean
Download exact raw UTF-8 source
1import MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Convex2import Mathlib.Analysis.Normed.Module.Connected3import Mathlib.Analysis.Normed.Module.RCLike.Real45/-!6# Ball extension corollaries78The closed-ball theorem first transports the center using the bounded9point-reflection theorem, then applies the convex ambient-interior corollary.10-/1112open Metric Set AffineIsometryEquiv Bornology1314namespace MathlibAnnex1516noncomputable section1718variable {E F : Type*}19 [NormedAddCommGroup E] [NormedSpace ℝ E]20 [NormedAddCommGroup F] [NormedSpace ℝ F]2122namespace IsometryEquiv2324/-- A surjective isometry between positive-radius open balls extends to a25unique ambient real affine isometry equivalence. -/26theorem existsUnique_affineExtension_ball27 {c : E} {d : F} {r R : ℝ} (f : ball c r ≃ᵢ ball d R)28 (hr : 0 < r) (hR : 0 < R) :29 ∃! A : E ≃ᵃⁱ[ℝ] F,30 ∀ x : ball c r, A (x : E) = ((f x : ball d R) : F) := by31 have _htc : IsConnected (ball d R) := isConnected_ball hR32 exact MathlibAnnex.IsometryEquiv.existsUnique_affineExtension33 f isOpen_ball (isConnected_ball hr) isOpen_ball3435private theorem pointReflection_mapsTo_closedBall (c : E) (r : ℝ) :36 MapsTo (pointReflection ℝ c) (closedBall c r) (closedBall c r) := by37 intro x hx38 rw [mem_closedBall, dist_pointReflection_fixed]39 exact hx4041/-- A surjective isometry between closed balls of the same positive radius42extends to a unique ambient real affine isometry equivalence. -/43theorem existsUnique_affineExtension_closedBall44 {c : E} {d : F} {r : ℝ} (f : closedBall c r ≃ᵢ closedBall d r)45 (hr : 0 < r) :46 ∃! A : E ≃ᵃⁱ[ℝ] F,47 ∀ x : closedBall c r,48 A (x : E) = ((f x : closedBall d r) : F) := by49 let cc : closedBall c r := ⟨c, mem_closedBall_self hr.le⟩50 let dd : closedBall d r := ⟨d, mem_closedBall_self hr.le⟩51 have hcenter : f cc = dd :=52 MathlibAnnex.IsometryEquiv.map_center_of_reflectionInvariant53 f cc.property dd.property isBounded_closedBall54 (pointReflection_mapsTo_closedBall c r)55 (pointReflection_mapsTo_closedBall d r)56 have hcenter_val : ((f cc : closedBall d r) : F) = d :=57 congrArg Subtype.val hcenter58 have hfi : ∀ x : closedBall c r,59 (x : E) ∈ interior (closedBall c r) ↔60 ((f x : closedBall d r) : F) ∈ interior (closedBall d r) := by61 intro x62 rw [interior_closedBall c hr.ne', interior_closedBall d hr.ne',63 mem_ball, mem_ball]64 have hdist : dist ((f x : closedBall d r) : F) d = dist (x : E) c := by65 calc66 dist ((f x : closedBall d r) : F) d =67 dist ((f x : closedBall d r) : F)68 ((f cc : closedBall d r) : F) := by rw [hcenter_val]69 _ = dist (f x) (f cc) := rfl70 _ = dist x cc := f.dist_eq x cc71 _ = dist (x : E) c := rfl72 rw [hdist]73 have hsint : (interior (closedBall c r)).Nonempty := by74 rw [interior_closedBall c hr.ne']75 exact nonempty_ball.mpr hr76 exact77 MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex78 f (convex_closedBall c r) hsint hfi7980end IsometryEquiv8182end8384end MathlibAnnex