OAI/Analysis/CircleDomains/Sobolev/PhysicalPartitionBands.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The quotient-band consequence of a physical positive sampling partition.

  1. theorem OAI.CircleDomainRigidity.physical_partition_band_inclusion line 17