support_subset_source — Mathlib · SciLib

English

The support of f is contained in the chart source: support(f) ⊆ chartAt(H,c).source.

Русский

Опорное множество f содержится в области источника диаграммы: supp(f) ⊆ chartAt(H,c).source.

LaTeX

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

Lean4

theorem support_subset_source : support f ⊆ (chartAt H c).source := by
  rw [f.support_eq_inter_preimage, ← extChartAt_source I]; exact inter_subset_left

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