tsupport_subset_extChartAt_source

English

Let f be a SmoothBumpFunction I c. Then the support tsupport(f) lies inside the chart source extChartAt I c.

Русский

Пусть f — гладкая выпуклая функция-амплитуда, центрированная в c. Поддержка tsupport(f) содержится в области определения экст-chartAt I c.

LaTeX

$$$\operatorname{tsupport}(f) \subseteq (\operatorname{extChartAt} I c).\text{source}$$$

Lean4

theorem tsupport_subset_extChartAt_source : tsupport f ⊆ (extChartAt I c).source :=
  calc
    tsupport f ⊆ (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) :=
      f.tsupport_subset_symm_image_closedBall
    _ ⊆ (extChartAt I c).symm '' (extChartAt I c).target := (image_mono f.closedBall_subset)
    _ = (extChartAt I c).source := (extChartAt I c).symm_image_target_eq_source

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