ClosedGermExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Bernoulli.LocalExtension.exists_contDiff_one_of_closed_germs line 17
Source documentation
C1 germs agreeing on a closed subset glue to a global C1 extension. This is an application of the actual smooth partition of unity, not a Whitney extension premise.
```
lemma exists_contDiff_one_of_closed_germs {S:Set E} (hS:IsClosed S) {F:E→G}
    (hg:∀x∈S,∃B:E→G,ContDiffAt ℝ 1 B x ∧ ∀ᶠ y in 𝓝 x,y∈S→B y=F y) :
    ∃B:E→G,ContDiff ℝ 1 B ∧ EqOn B F S := by
…
```