High-contrast homogenization: Provider.PolynomialHomogenization.EuclideanBallDistance #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Euclidean balls in distance form #
theorem
HCPolySupport.HighContrast.mem_euclideanBallAt_iff_euclideanDist_lt
{d : ℕ}
{c x : Vec d}
{r : ℝ}
(hr : 0 < r)
:
Membership in euclideanBallAt is equivalently a strict Euclidean
distance bound when the radius is positive.