OAI/Analysis/CircleDomains/Topology/JoinedAllowedPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The binary join is allowed, with its tags constructed from one original path and affine restrictions of the other.

  1. theorem OAI.CircleDomainRigidity.exists_allowed_joined_path line 22