Sorts

Points

WorldView

Functions

WorldLine

Translations

AxSelfMinus

TangentLines

Cones

AxLightMinus

Proposition1

AxEField

Norms

AxTriangleInequality

Sublemma3

Vectors

CauchySchwarz

Matrices

LinearMaps

Affine

Sublemma4

MainLemma

AxDiff

TangentLineLemma

Proposition2

AxEventMinus

Proposition3

ObserverConeLemma

Quadratics

Classification

ReverseCauchySchwarz

KeyLemma

Cardinalities

AffineConeLemma

NoFTLGR