Theorems · Theorem · global analysis

Continuous.exists_contMDiff_approx_and_eqOn

∀ {E : Type u_1} {F : Type u_2} {H : Type u_3} {M : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I (↑⊤) M]
  [SigmaCompactSpace M] [T2Space M] {f : M → F} {ε : M → ℝ} (n : ℕ∞),
  Continuous f →
    Continuous ε →
      (∀ (x : M), 0 < ε x) →
        ∀ {S U : Set M},
          IsClosed S →
            U ∈ nhdsSet S →
              ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) f U →
                ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ Set.EqOn (⇑g) f S ∧ Function.support ⇑g ⊆ Function.support f

Defined in

Mathlib.Geometry.Manifold.SmoothApprox

Cited by

2 results in Mathlib

Foundations

Depth 300 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldSigmaCompactSpaceT2Space