OAI/Probability/SLE/Geometry/SymmetricChartUpperBijective.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Restricting a symmetric disk chart to its upper component preserves surjectivity onto the upper half disk.

  1. theorem OAI.SLEExactGauge.symmetric_disk_chart_upper_bijOn line 13