OAI/Analysis/CircleDomains/Sobolev/ShrinkingRectanglePartition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A countable compact smooth partition subordinate to coordinate rectangles with the distance-to-dust sampling control.

  1. theorem OAI.CircleDomainRigidity.exists_shrinking_rectangle_partition line 16