OAI/Analysis/CircleDomains/Modulus/SelectedBarrierRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A small barrier is compatible with any subfamily of its retained levels.

  1. theorem OAI.CircleDomainRigidity.GradedRealTest.exists_compatible_of_small_barrier line 19