LeanPool.Rupert.Basic

Imported Lean Pool material for LeanPool.Rupert.Basic.

def «termℝ³» : Lean.ParserDescr

Three-dimensional Euclidean space over ℝ.

Equations

• «termℝ³» = Lean.ParserDescr.node `«termℝ³» 1024 (Lean.ParserDescr.symbol "ℝ³")

def «termℝ²» : Lean.ParserDescr

Two-dimensional Euclidean space over ℝ.

Equations

• «termℝ²» = Lean.ParserDescr.node `«termℝ²» 1024 (Lean.ParserDescr.symbol "ℝ²")

@[reducible, inline]

abbrev E (n : ℕ) : Type

n-dimensional Euclidean space over ℝ, indexed by Fin n.

Equations

• E n = EuclideanSpace ℝ (Fin n)

@[reducible, inline]

abbrev SO3 : Submonoid (Matrix (Fin 3) (Fin 3) ℝ)

The special orthogonal group in dimension three over ℝ.

Equations

• SO3 = Matrix.specialOrthogonalGroup (Fin 3) ℝ

def projXy {k : Type} (v : EuclideanSpace k (Fin 3)) : EuclideanSpace k (Fin 2)

Projects a vector from 3-space to 2-space by dropping the third coordinate.

Equations

• projXy v = !₂[v.ofLp 0, v.ofLp 1]

def IsRupert {ι : Type} (vertices : ι → ℝ³) : Prop

The Rupert Property for a convex polyhedron given as an indexed finite set of vertices.

Equations

• One or more equations did not get rendered due to their size.

def IsRupert' {ι : Type} (vertices : ι → ℝ³) : Prop

Alternate formulation of the Rupert Property. This is equivalent to IsRupert and should be easier to prove.

Equations

• One or more equations did not get rendered due to their size.