InitialInverseCommonDomain.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Every inverse-chart limit covers the common final slit domain. No convergence of the times, nor a boundary driving value, is assumed here.

theorem OAI.SLEExactGauge.initialInverse_limit_covers_final_domain line 15