OAI/Analysis/CircleDomains/Topology/FillingDisks.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite filling disks for a finite grid family

Descending induction on the labels constructs pairwise disjoint smooth physical disks covering relatively clopen dust. Each boundary meets at most one grid. The singleton-component hypothesis is exactly the lower-obstacle conclusion proved in GridObstacles; no contour-selection hypothesis is assumed here.

  1. theorem OAI.CircleDomainRigidity.exists_finite_filling_disks line 21