OAI/Analysis/CircleDomains/Topology/RankedTagTopology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Free tag contacts are excluded by the largest inherited label in a finite tuple, irrespective of the enumeration used to encode the tuple.

  1. theorem OAI.CircleDomainRigidity.tag_impossible_below_ranked_level line 14
  2. theorem OAI.CircleDomainRigidity.incompatible_ranked_tag_pair_at_point line 49