OAI/Analysis/CircleDomains/Topology/CircleLiftTransitions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous real branches of one circle coordinate differ locally by a constant integer. Their ordinary derivatives therefore agree.

  1. theorem OAI.CircleDomainRigidity.circle_lift_difference_eventually_constant line 14
  2. theorem OAI.CircleDomainRigidity.circle_lift_difference_contDiffAt line 31
  3. theorem OAI.CircleDomainRigidity.circle_lift_difference_eq_on_preconnected line 41
  4. theorem OAI.CircleDomainRigidity.contDiffAt_circle_quotient_chart line 55