mem_chartAt_ind_source — Mathlib

English

If f is a SmoothBumpCovering subordinate to U, then the induced chart neighbourhoods contain the supports of bumps.

Русский

Если f -- SmoothBumpCovering, подчинённое U, то области диаграмм содержат опоры бамп-функций.

LaTeX

$$∀ i, tsupport(f i) ⊆ U (f c i)$$

Lean4

theorem mem_chartAt_ind_source (x : M) (hx : x ∈ s) : x ∈ (chartAt H (fs.c (fs.ind x hx))).source :=
  fs.mem_chartAt_source_of_eq_one (fs.apply_ind x hx)

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