OAI/Analysis/CircleDomains/Selection/RoundHoleOffsets.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A single positive offset works for a finite family of disjoint round holes. The enlarged closed holes remain disjoint and inside the given open region, including when an original hole has radius zero.

  1. theorem OAI.CircleDomainRigidity.exists_common_round_hole_offset line 15