theorem Noperthedron.c1_norm_oneNoperthedron.c1_norm_one : ‖C1R‖ = 1 : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. C1RNoperthedron.C1R : Euc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1

theorem Noperthedron.c2_norm_boundNoperthedron.c2_norm_bound : ‖C2R‖ ∈ Set.Ioo (98 / 100) (99 / 100) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. C2RNoperthedron.C2R : Euc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IooSet.Ioo.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioo a b` is the left-open right-open interval $(a, b)$.  (98 / 100) (99 / 100)

theorem Noperthedron.c3_norm_boundNoperthedron.c3_norm_bound : ‖C3R‖ ∈ Set.Ioo (98 / 100) (99 / 100) :
  ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. C3RNoperthedron.C3R : Euc(3)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Set.IooSet.Ioo.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioo a b` is the left-open right-open interval $(a, b)$.  (98 / 100) (99 / 100)

theorem Noperthedron.exactVertex_radius_oneNoperthedron.exactVertex_radius_one : { v := exactVertex }.radius = 1The radius of the noperthedron is 1.
 :
  {Polyhedron.mk {ι X : Type} (v : ι → X) : Polyhedron ι X vVertexIndex → Euc(3) :=Polyhedron.mk {ι X : Type} (v : ι → X) : Polyhedron ι X exactVertexNoperthedron.exactVertex (idx : VertexIndex) : Euc(3) }Polyhedron.mk {ι X : Type} (v : ι → X) : Polyhedron ι X.radiusPolyhedron.radius {ι X : Type} [Fintype ι] [ne : Nonempty ι] [Norm X] (p : Polyhedron ι X) : ℝ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1

theorem Noperthedron.exactVertex_norm_le_oneNoperthedron.exactVertex_norm_le_one (j : VertexIndex) : ‖exactVertex j‖ ≤ 1
  (jVertexIndex : VertexIndexNoperthedron.VertexIndex : TypeIdentifier for a Noperthedron vertex.
Corresponds to the point at `(-1)^ℓ • Rz(2π k / 15) (C i)`
) : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. exactVertexNoperthedron.exactVertex (idx : VertexIndex) : Euc(3) jVertexIndex‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1

theorem Noperthedron.exactPoly_point_symmetricNoperthedron.exactPoly_point_symmetric : PointSym exactPoly.hullThe noperthedron is pointsymmetric.
 :
  PointSymPointSym {n : ℕ} (A : Set Euc(n)) : Prop exactPolyNoperthedron.exactPoly : GoodPoly VertexIndex.hullGoodPoly.hull {ι : Type} [Fintype ι] [Nonempty ι] (poly : GoodPoly ι) : Set Euc(3)

theorem Noperthedron.Tightening.lemma7_1Noperthedron.Tightening.lemma7_1 (θ φ : ℝ) :
  ⇑(rotM (θ + 2 / 15 * Real.pi) φ) '' exactPolyhedron.hull = ⇑(rotM θ φ) '' exactPolyhedron.hull
  (θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  ⇑(rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.θℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. 2 / 15 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened. )HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. φℝ) ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. 
      exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    ⇑(rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ) ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`.  exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Tightening.lemma7_2Noperthedron.Tightening.lemma7_2 (θ φ α : ℝ) :
  ⇑(rotR (α + Real.pi)) ∘ ⇑(rotM θ φ) '' exactPolyhedron.hull = ⇑(rotR α) ∘ ⇑(rotM θ φ) '' exactPolyhedron.hull
  (θℝ φℝ αℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  ⇑(rotRrotR : AddChar ℝ (Euc(2) →L[ℝ] Euc(2)) (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.αℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened. )HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.) ∘Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δFunction composition, usually written with the infix operator `∘`. A new function is created from
two existing functions, where one function's output is used as input to the other.

Examples:
 * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`
 * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`


Conventions for notations in identifiers:

 * The recommended spelling of `∘` in identifiers is `comp`. ⇑(rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ) ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. 
      exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    ⇑(rotRrotR : AddChar ℝ (Euc(2) →L[ℝ] Euc(2)) αℝ) ∘Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δFunction composition, usually written with the infix operator `∘`. A new function is created from
two existing functions, where one function's output is used as input to the other.

Examples:
 * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`
 * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`


Conventions for notations in identifiers:

 * The recommended spelling of `∘` in identifiers is `comp`. ⇑(rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ) ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. 
      exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Tightening.lemma7_3Noperthedron.Tightening.lemma7_3 (θ φ : ℝ) :
  ⇑(flip_y.comp (rotM θ φ)) '' exactPolyhedron.hull = ⇑(rotM (θ + Real.pi / 15) (Real.pi - φ)) '' exactPolyhedron.hull
  (θℝ φℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  ⇑(flip_yflip_y : Euc(2) →L[ℝ] Euc(2).compContinuousLinearMap.comp.{u_1, u_2, u_3, u_4, u_6, u_7} {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁]
  [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4}
  [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7}
  [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : M₁ →SL[σ₁₃] M₃Composition of bounded linear maps.  (rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) θℝ φℝ)) ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. 
      exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    ⇑(rotMrotM (θ φ : ℝ) : Euc(3) →L[ℝ] Euc(2) (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.θℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.  /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. 15)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
          (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.  -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). φℝ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).) ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. 
      exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Tightening.rupert_tighteningNoperthedron.Tightening.rupert_tightening (p : Pose ℝ) (r : RupertPose p exactPolyhedron.hull) :
  ∃ p', tightInterval.contains p' ∧ RupertPose p' exactPolyhedron.hull
  (pPose ℝ : PosePose (R : Type) : Type ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (rRupertPose p exactPolyhedron.hull :
    RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 pPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)) :
  ∃ p'Pose ℝ,
    tightIntervaltightInterval : PoseInterval ℝThe 5d box in parameter space that represents what constraints we can
impose on angles taking advantage of the particular symmetries of the
Noperthedron.
.containsPoseInterval.contains {R : Type} [PartialOrder R] (iv : PoseInterval R) (vp : Pose R) : Prop`iv.contains p` ↔ `p ∈ Set.Icc iv.min iv.max` ↔ `p ∈ iv`. Provided as a
named alias for legibility at call sites; `iv.contains p` and `p ∈ iv` are
definitionally equal.  p'Pose ℝ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 p'Pose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)