ComplexLipschitzExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous extension of a complex Lipschitz map from a time set. The coordinatewise real extensions suffice for the raw flow endpoint.