OAI/Analysis/CircleDomains/Topology/TagComponents.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nonconstant active tag lies in a nontrivial connected component through each of its interior image points.

  1. theorem OAI.CircleDomainRigidity.nontrivial_component_of_tag line 18
  2. theorem OAI.CircleDomainRigidity.active_tag_nontrivial_component line 41