`BookProof.ChapterFreeFieldBornCont.bornMap_mapsTo_stdSimplex` : Set.MapsTo (bornMap : EuclideanSpace ℝ (Fin n) → (Fin n → ℝ)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1) (std

Initializing...

`BookProof.ChapterFreeFieldBornCont.bornMap_mapsTo_stdSimplex` : Set.MapsTo (bornMap : EuclideanSpace ℝ (Fin n) → (Fin n → ℝ)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1) (std · Prove2Me