exists_isSubordinate_chartAt_source_of_isClosed

English

A smooth partition subordinate to an open chart source exists.

Русский

Существует гладкое разбиение единиц, подчинённое открытым источникам чартов.

LaTeX

$$$\\exists f: SmoothPartitionOfUnity, f.IsSubordinate (chartAt H x).source$$$

Lean4

theorem exists_isSubordinate_chartAt_source_of_isClosed {s : Set M} (hs : IsClosed s) :
    ∃ f : SmoothPartitionOfUnity s I M s, f.IsSubordinate (fun x ↦ (chartAt H (x : M)).source) :=
  by
  apply exists_isSubordinate _ hs _ (fun i ↦ (chartAt H _).open_source) (fun x hx ↦ ?_)
  exact mem_iUnion_of_mem ⟨x, hx⟩ (mem_chart_source H x)

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