OAI/Analysis/CircleDomains/Topology/OpenGraphHausdorff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Remove the fixed interior margin by a compact exhaustion of the open energy neighborhood. The resulting estimate applies to the entire set.

  1. lemma OAI.CircleDomainRigidity.local_graph_hausdorff_le_open line 14