OAI/Analysis/CircleDomains/Selection/EndCluster.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cluster values at a specified end

The matched side identity places images of a sequence approaching the source end eventually in every target collar. A convergent image sequence therefore limits in the full target component, without extending the map across that component.

  1. theorem OAI.CircleDomainRigidity.cluster_mem_matched_end line 21
  2. theorem OAI.CircleDomainRigidity.cluster_mem_corresponding_component line 42