OAI/Analysis/CircleDomains/Topology/TagPairTopology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The topological part of excluding free contacts of two tags. At the largest level label present at a contact, the other tag gives a forbidden nontrivial component in lower levels.

  1. theorem OAI.CircleDomainRigidity.tag_impossible_below_compatible_level line 18
  2. theorem OAI.CircleDomainRigidity.incompatible_tag_pair_at_point line 52