OAI/Probability/SLE/Stochastic/PlanarLogLifting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Elementary lifting facts used to prove the planar disk openness input. An odd nonzero function on a connected antipodal space cannot have a continuous logarithm.

  1. lemma OAI.SLEExactGauge.continuous_log_at_end_of_homotopy line 16
  2. lemma OAI.SLEExactGauge.no_continuous_log_of_odd_involution line 29