LeanPool.Rupert.Set

Imported Lean Pool material for LeanPool.Rupert.Set.

def IsRupertPair (inner outer : Set ℝ³) : Prop

The Rupert Property for a pair of subsets X, Y of ℝ³. X has the Rupert property with respect to Y if there such that the shadow of X fits "comfortably" within the shadow of Y under affine transformations. By "comfortably" we mean the closure of one set is a subset of the interior of the other. This definition rules out trivial cases of a set fitting inside itself.

Equations

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

def IsRupertSet (S : Set ℝ³) : Prop

The Rupert Property for a subset S of ℝ³. S has the Rupert property if there are rotations and translations such that one 2-dimensional "shadow" of S can be made to fit entirely inside the interior of another such "shadow".

Equations

• IsRupertSet S = IsRupertPair S S