OAI/Analysis/CircleDomains/Transfer/RegularImageCircuit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual image of a regular source circuit is regular. No orientation choice is needed here: the inverse differential prevents zero tangents.

  1. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.regular_image_circuit line 15