LeanPool.Rupert.Affine #
Imported Lean Pool material for LeanPool.Rupert.Affine.
def
IsAffineRupertPair
{P : Type u_1}
{V : Type u_2}
[MetricSpace P]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddTorsor V P]
[FiniteDimensional ℝ V]
(inner outer : Set P)
:
The Rupert Property for a pair of subsets X, Y of an arbitrary finite-dimensional real affine space P. X has the Rupert property with respect to Y if there exist
- affine isometries transforming X and Y respectively
- an maximal nontrivial affine subspace Q of P such that the orthogonal projection onto Q of the transformed image of X fits "comfortably" within the projection onto Q of the transformed image of Y.
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.
Instances For
def
IsAffineRupertSet
{P : Type u_1}
{V : Type u_2}
[MetricSpace P]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddTorsor V P]
[FiniteDimensional ℝ V]
(S : Set P)
:
The Rupert Property for a subset S of affine space P. S has the Rupert property if it has the pairwise Rupert property with respect to itself.