SphereTransport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EuclideanRamsey.cospherical_transport line 14
Source documentation
A full-affine-span representative transfers its sphere to any congruent configuration. The translated linear isometry preserves the radius exactly; in particular, there is no rescaling of the pairwise distances. No injectivity or positive-dimension hypothesis is needed for this transport lemma.
```
theorem cospherical_transport {s D d : ℕ}
    (a : Fin s → Space D) (b : Fin s → Space d)
    (hspan : affineSpan ℝ (Set.range b) = ⊤)
    (hab : Congruent a b)
    (hb : EuclideanGeometry.Cospherical (Set.range b)) :
    EuclideanGeometry.Cospherical (Set.range a) := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.Congruent