OAI/Analysis/CircleDomains/Rigidity/CountableMatchedComponents.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The exceptional component pairs in the trace argument are countable: one side has nonempty interior. Common point pairs remain unrestricted.

  1. theorem OAI.CircleDomainRigidity.IsComplementaryComponent.eq_component_of_mem line 15
  2. theorem OAI.CircleDomainRigidity.circle_component_euclidean line 21
  3. theorem OAI.CircleDomainRigidity.circle_component_singleton_or_interior line 38
  4. def OAI.CircleDomainRigidity.MatchedConformalEnds.IsMatchedComponentPair line 57
  5. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.IsMatchedComponentPair.fst_injective line 61
  6. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.equal_target_fibers_equal_source_components line 67
  7. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.IsMatchedComponentPair.snd_injective line 86
  8. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.exists_matched_pair_of_source line 103
  9. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.exists_matched_pair_of_target line 113
  10. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.matched_pair_indexed_or_common_point line 129
  11. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.countable_matched_nonpoint_components line 141