FillRegionBands.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Filling an open region by one cannot enlarge a boundary band at any point away from the region's frontier. This assertion is pointwise.