OAI/Analysis/CircleDomains/Selection/MappedPointAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Point avoidance passes to the actual compact disk-arc image law. Injectivity is required only on each sampled arc together with the single point under consideration.

  1. theorem OAI.CircleDomainRigidity.mapped_arc_point_avoidance line 16