OAI/Analysis/CircleDomains/Selection/ScaledGraphCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Affine dilation of a graph cover retains its diameter and cost factors. The metric is the sup metric on the base and the vertical axis.

  1. def OAI.CircleDomainRigidity.graphAffine line 13
  2. lemma OAI.CircleDomainRigidity.graphAffine_lipschitz line 16
  3. lemma OAI.CircleDomainRigidity.scaled_graph_cover line 23