LocalSmoothExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A smooth map whose value and differential vanish at the origin has a compactly supported small ambient extension on a sufficiently small disk.

lemma OAI.CircleDomainRigidity.exists_smooth_local_error_extension line 12