mem_extChartAt_ind_source

Mathlib.Geometry.Manifold.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#SmoothBumpCovering.mem_extChartAt_ind_source

← MathLib Explorer

English

If f is subordinate to U, then the extChartAt neighborhoods cover tsupports.

Русский

Если f подчинено U, то окрестности extChartAt охватывают tsupport.

LaTeX

$$∀ i, x, x ∈ tsupport(f_i) ⇒ x ∈ extChartAt(I, f.c i).source$$

Lean4

theorem mem_extChartAt_ind_source (x : M) (hx : x ∈ s) : x ∈ (extChartAt I (fs.c (fs.ind x hx))).source :=
  fs.mem_extChartAt_source_of_eq_one (fs.apply_ind x hx)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru