Exact source: MathlibAnnex/Analysis/Normed/Sphere/ModelTransport.lean
Pinned GitHub source · Raw UTF-8 source
Back to The unit-sphere chord metric determines the ambient normed space
1import MathlibAnnex.Analysis.Normed.Plucker.ModelRigidity2import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Transport3import MathlibAnnex.Analysis.Normed.Sphere.Dimension45noncomputable section6set_option autoImplicit false7open Set8universe u v910namespace MathlibAnnex.Sphere11/-- Transport the accepted model theorem through any common finite coordinate system. -/12theorem nonempty_linearIsometryEquiv_of_coordinate_model13 {m : ℕ} {X : Type u} {Y : Type v}14 [NormedAddCommGroup X] [NormedSpace ℝ X]15 [NormedAddCommGroup Y] [NormedSpace ℝ Y]16 (Δ : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)17 (eX : (Fin (m + 1) → ℝ) ≃L[ℝ] X)18 (eY : (Fin (m + 1) → ℝ) ≃L[ℝ] Y) : Nonempty (X ≃ₗᵢ[ℝ] Y) := by19 let MX := EquivalentSeminorm.ofContinuousLinearEquiv eX20 let MY := EquivalentSeminorm.ofContinuousLinearEquiv eY21 let ΔM := EquivalentSeminorm.sphereIsometryEquiv eX eY Δ22 rcases EquivalentSeminorm.nonempty_linearIsometryEquiv_of_sphereIsometryEquiv MX MY ΔM with ⟨A⟩23 exact ⟨EquivalentSeminorm.transportLinearIsometryEquiv eX eY A⟩24end MathlibAnnex.Sphere