OAI/Analysis/CircleDomains/Modulus/CodeFreeIncidence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Combining the actual residual constraints with null incidence sets on the open tags needs no globally chosen circle trace.

  1. theorem OAI.CircleDomainRigidity.ae_code_free_level_incidence_null_of_tags line 17