LeanPool.Rupert.Square

Imported Lean Pool material for LeanPool.Rupert.Square.

@[reducible, inline]

abbrev Square.vertices : Fin 4 → ℝ³

A square in the xy-plane, centered at the origin and with side length 2.

Equations

• Square.vertices = ![!₂[-1, -1, 0], !₂[1, -1, 0], !₂[-1, 1, 0], !₂[1, 1, 0]]

noncomputable def Square.rh : ℝ

square root of one-half

Equations

• Square.rh = √2 / 2

theorem Square.rh_lemma : rh * rh + rh * rh = 1

@[reducible, inline]

abbrev Square.innerRot : Matrix (Fin 3) (Fin 3) ℝ

Rotation matrix for the inner square shadow.

Equations

• Square.innerRot = !![1, 0, 0; 0, 0, -1; 0, 1, 0]

theorem Square.innerRot_so3 : innerRot ∈ SO3

@[reducible, inline]

noncomputable abbrev Square.outerRot : Matrix (Fin 3) (Fin 3) ℝ

Rotation matrix for the outer square shadow.

Equations

• Square.outerRot = !![Square.rh, Square.rh, 0; -Square.rh, Square.rh, 0; 0, 0, 1]

theorem Square.outerRot_so3 : outerRot ∈ SO3

theorem Square.square_is_rupert : IsRupert vertices