AcrossSmall #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.across_small
{T : Configuration}
{r s : ℝ}
(H : Canonical ContactCase.Across T r s)
(hs : s ≤ 1 / 80)
:
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.