tsupport_mem_nhds — Mathlib

English

For any closed s ⊆ support f, there exists r with 0 < r < f.rOut such that s ⊆ chart source ∩ extChartAt⁻¹'ball(..., r).

Русский

Для любого замкнутого s ⊆ support f существует r с 0 < r < f.rOut и s ⊆ chart source ∩ extChartAt⁻¹' ball(..., r).

LaTeX

$$$\exists r \in (0, f.rOut)\;\text{such that } s \subseteq (chartAt H c).source \cap extChartAt I c^{-1}(\mathrm{ball}(\operatorname{extChartAt} I c c, r)).$$$

Lean4

theorem tsupport_mem_nhds : tsupport f ∈ 𝓝 c :=
  mem_of_superset f.support_mem_nhds subset_closure

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