OAI/Analysis/CircleDomains/Selection/TagPairAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ordered compatibility and tuple absolute continuity exclude every free contact between two independent active tags.

  1. theorem OAI.CircleDomainRigidity.ae_no_tag_pair_contact line 19