OAI/Geometry/Arnold/Extension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ArnoldCounterexample.Extension.contDiff_mul_of_tsupport_subset line 19
2. theorem OAI.ArnoldCounterexample.Extension.global_extension line 34

   Source documentation

   Local ambient smooth extensions glue globally on a compact subset of a finite-dimensional real vector space. No extension theorem is assumed.

   theorem global_extension {K : Set E} (hK : IsCompact K) (f : K → ℝ)
       (hlocal : ∀ z : K, ∃ U : Set E, ∃ g : E → ℝ,
         IsOpen U ∧ ↑z ∈ U ∧ ContDiffOn ℝ ∞ g U ∧ ∀ y : K, ↑y ∈ U → g y = f y) :
       ∃ G : E → ℝ, ContDiff ℝ ∞ G ∧ ∀ z : K, G z = f z := by
   …