GeometryDefinitions.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ProjectionCounterexample.E line 11
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:15 (same declaration text).
def OAI.ProjectionCounterexample.simplex line 14
Source documentation
The convex hull of the origin and the d standard unit vectors.
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:17 (same declaration text).
```
def simplex (d : ℕ) : Set (E d) :=
…
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.firstBlock line 18
Source documentation
The first ten coordinates in the standard orthogonal decomposition of R²⁰.
```
def firstBlock (x : E 20) : E 10 :=
…
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.secondBlock line 22
Source documentation
The last ten coordinates in the standard orthogonal decomposition of R²⁰.
```
def secondBlock (x : E 20) : E 10 :=
…
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.productBody line 26
Source documentation
The genuine Cartesian product T₁₀ × T₁₀ in Euclidean R²⁰.
```
def productBody : Set (E 20) :=
…
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.IsConvexBody line 30
Source documentation
Compact, convex, and full-dimensional in its specified Euclidean space.
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:20 (same declaration text).
```
def IsConvexBody {d : ℕ} (P : Set (E d)) : Prop :=
…
```
Mentions: OAI.ProjectionCounterexample.E