contMDiff — Mathlib

English

The same as nhds_basis_tsupport; the neighborhoods basis is given by tsupports.

Русский

То же самое, что и nhds_basis_tsupport; база окрестностей строится из tsupport.

LaTeX

$$$(\nhds c).HasBasis (\lambda f : SmoothBumpFunction I c, True) (\lambda f, \operatorname{tsupport}(f))$$

Lean4

/-- A smooth bump function is infinitely smooth. -/
protected theorem contMDiff : ContMDiff I 𝓘(ℝ) ∞ f :=
  by
  refine contMDiff_of_tsupport fun x hx => ?_
  have : x ∈ (chartAt H c).source := f.tsupport_subset_chartAt_source hx
  refine
    ContMDiffAt.congr_of_eventuallyEq ?_ <| f.eqOn_source.eventuallyEq_of_mem <| (chartAt H c).open_source.mem_nhds this
  exact f.contDiffAt.contMDiffAt.comp _ (contMDiffAt_extChartAt' this)

Похожие утверждения