OAI/Probability/SLE/Geometry/StrictRealLocalChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A reflection-symmetric analytic germ tangent to the identity preserves the upper side in a sufficiently small neighborhood.

  1. lemma OAI.SLEExactGauge.strict_real_germ_maps_upper line 14