tsupport_subset_chartAt_source — Mathlib

English

For a bump function f, tsupport(f) is contained in the source of the chart chartAt H c.

Русский

Для функции-выпуклости f область поддержки лежит внутри области определения карты chartAt H c.

LaTeX

$$$\operatorname{tsupport}(f) \subseteq (\operatorname{chartAt} H c).\text{source}$$$

Lean4

theorem tsupport_subset_chartAt_source : tsupport f ⊆ (chartAt H c).source := by
  simpa only [extChartAt_source] using f.tsupport_subset_extChartAt_source

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