OAI/Analysis/CircleDomains/Topology/ConnectedSetPolygonalApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite metric chains give actual ambient paths arbitrarily close to a connected set. These are the paths to be refined in the compact arc argument.

  1. lemma OAI.CircleDomainRigidity.metric_chain_path_near_set line 14
  2. lemma OAI.CircleDomainRigidity.connected_set_path_near line 39