`BookProof.ChapterG2.gauge_fixing_section_discontinuous` (s : Circle → ℝ) (hs : ∀ z, Circle.exp (s z) = z) : ¬ Continuous s

Initializing...

`BookProof.ChapterG2.gauge_fixing_section_discontinuous` (s : Circle → ℝ) (hs : ∀ z, Circle.exp (s z) = z) : ¬ Continuous s · Prove2Me