OAI/Analysis/CircleDomains/Topology/AllowedPathRestriction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual affine restriction of an allowed tagged path is allowed. The only level hypothesis is the pointwise incidence bound already required of the level weights. No path-stability statement is assumed.

  1. theorem OAI.CircleDomainRigidity.allowedTaggedPath_affine line 22