MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex
theorem existsUnique_affineExtension_of_convex
{s : Set E} {t : Set F} (f : s ≃ᵢ t)
(hs : Convex ℝ s) (hsint : (interior s).Nonempty)
(hfi : ∀ x : s,
(x : E) ∈ interior s ↔ ((f x : t) : F) ∈ interior t) :
∃! A : E ≃ᵃⁱ[ℝ] F,
∀ x : s, A (x : E) = ((f x : t) : F)1 import MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.OpenConnected 2 import Mathlib.Analysis.Convex.Topology 3 4 /-! 5 # Convex-set extension corollary 6 7 The theorem in this module applies the open-connected extension theorem to 8 ambient interiors, then extends the agreement to the whole convex sets by 9 continuity and density. 10 -/ 11 12 open Metric Set 13 14 namespace MathlibAnnex 15 16 noncomputable section 17 18 variable {E F : Type*} 19 [NormedAddCommGroup E] [NormedSpace ℝ E] 20 [NormedAddCommGroup F] [NormedSpace ℝ F] 21 22 namespace IsometryEquiv 23 24 private def interiorRestriction 25 {s : Set E} {t : Set F} (f : s ≃ᵢ t) 26 (hfi : ∀ x : s, (x : E) ∈ interior s ↔ ((f x : t) : F) ∈ interior t) : 27 interior s ≃ᵢ interior t where 28 toFun x := 29 ⟨((f ⟨x, interior_subset x.property⟩ : t) : F), 30 (hfi ⟨x, interior_subset x.property⟩).mp x.property⟩ 31 invFun y := by 32 let yt : t := ⟨y, interior_subset y.property⟩ 33 let xs : s := f.symm yt 34 refine ⟨(xs : E), ?_⟩ 35 apply (hfi xs).mpr 36 rw [show f xs = yt from f.apply_symm_apply yt] 37 exact y.property 38 left_inv x := by 39 apply Subtype.ext 40 change ((f.symm (f ⟨x, interior_subset x.property⟩) : s) : E) = (x : E) 41 exact congrArg Subtype.val (f.symm_apply_apply ⟨x, interior_subset x.property⟩) 42 right_inv y := by 43 apply Subtype.ext 44 change ((f (f.symm ⟨y, interior_subset y.property⟩) : t) : F) = (y : F) 45 exact congrArg Subtype.val (f.apply_symm_apply ⟨y, interior_subset y.property⟩) 46 isometry_toFun := Isometry.of_dist_eq fun x y => by 47 change dist (f ⟨x, interior_subset x.property⟩) 48 (f ⟨y, interior_subset y.property⟩) = dist x y 49 rw [f.dist_eq, Subtype.dist_eq, Subtype.dist_eq] 50 51 /-- An isometry equivalence from a convex set with nonempty ambient interior 52 extends uniquely if it preserves membership in the ambient interiors. 53 The target set is not separately assumed convex. -/ 54 theorem existsUnique_affineExtension_of_convex 55 {s : Set E} {t : Set F} (f : s ≃ᵢ t) 56 (hs : Convex ℝ s) (hsint : (interior s).Nonempty) 57 (hfi : ∀ x : s, 58 (x : E) ∈ interior s ↔ ((f x : t) : F) ∈ interior t) : 59 ∃! A : E ≃ᵃⁱ[ℝ] F, 60 ∀ x : s, A (x : E) = ((f x : t) : F) := by 61 let fi : interior s ≃ᵢ interior t := interiorRestriction f hfi 62 rcases MathlibAnnex.IsometryEquiv.existsUnique_affineExtension 63 fi isOpen_interior ((hs.interior).isConnected hsint) isOpen_interior with 64 ⟨A, hAi, hAuniq⟩ 65 let u : Set s := {x | (x : E) ∈ interior s} 66 have hu_image : Subtype.val '' u = interior s := by 67 ext z 68 constructor 69 · rintro ⟨w, hw, rfl⟩ 70 exact hw 71 · intro hz 72 exact ⟨⟨z, interior_subset hz⟩, hz, rfl⟩ 73 have hu_dense : Dense u := by 74 rw [Subtype.dense_iff, hu_image, 75 hs.closure_interior_eq_closure_of_nonempty_interior hsint] 76 exact subset_closure 77 have hAall : ∀ x : s, A (x : E) = ((f x : t) : F) := by 78 have hcontA : Continuous (fun x : s ↦ A (x : E)) := 79 A.continuous.comp continuous_subtype_val 80 have hcontf : Continuous (fun x : s ↦ ((f x : t) : F)) := 81 continuous_subtype_val.comp f.continuous 82 have heq : u.EqOn (fun x : s ↦ A (x : E)) 83 (fun x : s ↦ ((f x : t) : F)) := by 84 intro x hx 85 let xi : interior s := ⟨(x : E), hx⟩ 86 have h := hAi xi 87 exact h 88 exact fun x ↦ congrFun (Continuous.ext_on hu_dense hcontA hcontf heq) x 89 refine ⟨A, hAall, ?_⟩ 90 intro B hB 91 apply hAuniq 92 intro x 93 let xs : s := ⟨(x : E), interior_subset x.property⟩ 94 have h := hB xs 95 exact h 96 97 end IsometryEquiv 98 99 end 100 101 end MathlibAnnex