OAI/Analysis/CircleDomains/Sobolev/UniformLocalMollification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive mollification approximates a continuous branch uniformly on a compact set strictly inside its domain of continuity.

  1. theorem OAI.CircleDomainRigidity.planarMollification_uniform_on_compact line 14