Exact UTF-8 source: MathlibAnnex/Analysis/Normed/Affine/IsometryExtension/Convex.lean
Download exact raw UTF-8 source
1import MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.OpenConnected2import Mathlib.Analysis.Convex.Topology34/-!5# Convex-set extension corollary67The theorem in this module applies the open-connected extension theorem to8ambient interiors, then extends the agreement to the whole convex sets by9continuity and density.10-/1112open Metric Set1314namespace MathlibAnnex1516noncomputable section1718variable {E F : Type*}19 [NormedAddCommGroup E] [NormedSpace ℝ E]20 [NormedAddCommGroup F] [NormedSpace ℝ F]2122namespace IsometryEquiv2324private def interiorRestriction25 {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 where28 toFun x :=29 ⟨((f ⟨x, interior_subset x.property⟩ : t) : F),30 (hfi ⟨x, interior_subset x.property⟩).mp x.property⟩31 invFun y := by32 let yt : t := ⟨y, interior_subset y.property⟩33 let xs : s := f.symm yt34 refine ⟨(xs : E), ?_⟩35 apply (hfi xs).mpr36 rw [show f xs = yt from f.apply_symm_apply yt]37 exact y.property38 left_inv x := by39 apply Subtype.ext40 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 := by43 apply Subtype.ext44 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 => by47 change dist (f ⟨x, interior_subset x.property⟩)48 (f ⟨y, interior_subset y.property⟩) = dist x y49 rw [f.dist_eq, Subtype.dist_eq, Subtype.dist_eq]5051/-- An isometry equivalence from a convex set with nonempty ambient interior52extends uniquely if it preserves membership in the ambient interiors.53The target set is not separately assumed convex. -/54theorem existsUnique_affineExtension_of_convex55 {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) := by61 let fi : interior s ≃ᵢ interior t := interiorRestriction f hfi62 rcases MathlibAnnex.IsometryEquiv.existsUnique_affineExtension63 fi isOpen_interior ((hs.interior).isConnected hsint) isOpen_interior with64 ⟨A, hAi, hAuniq⟩65 let u : Set s := {x | (x : E) ∈ interior s}66 have hu_image : Subtype.val '' u = interior s := by67 ext z68 constructor69 · rintro ⟨w, hw, rfl⟩70 exact hw71 · intro hz72 exact ⟨⟨z, interior_subset hz⟩, hz, rfl⟩73 have hu_dense : Dense u := by74 rw [Subtype.dense_iff, hu_image,75 hs.closure_interior_eq_closure_of_nonempty_interior hsint]76 exact subset_closure77 have hAall : ∀ x : s, A (x : E) = ((f x : t) : F) := by78 have hcontA : Continuous (fun x : s ↦ A (x : E)) :=79 A.continuous.comp continuous_subtype_val80 have hcontf : Continuous (fun x : s ↦ ((f x : t) : F)) :=81 continuous_subtype_val.comp f.continuous82 have heq : u.EqOn (fun x : s ↦ A (x : E))83 (fun x : s ↦ ((f x : t) : F)) := by84 intro x hx85 let xi : interior s := ⟨(x : E), hx⟩86 have h := hAi xi87 exact h88 exact fun x ↦ congrFun (Continuous.ext_on hu_dense hcontA hcontf heq) x89 refine ⟨A, hAall, ?_⟩90 intro B hB91 apply hAuniq92 intro x93 let xs : s := ⟨(x : E), interior_subset x.property⟩94 have h := hB xs95 exact h9697end IsometryEquiv9899end100101end MathlibAnnex