High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryDistanceMonotone

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Monotonicity of boundary distance

Enlarging a domain can only increase distance to its complement.

theorem HCPolySupport.HighContrast.euclideanBoundaryDistance_mono {d : ℕ} {V U : Set (Vec d)} (hVU : V ⊆ U) (hUcompl : Uᶜ.Nonempty) (x : Vec d) : euclideanBoundaryDistance V x ≤ euclideanBoundaryDistance U x

Boundary distance is monotone with respect to inclusion of domains.