exists_isSubordinate_chartAt_source

English

There exists a SmoothPartitionOfUnity subordinate to chartAt sources for a given chart.

Русский

Существует SmoothPartitionOfUnity, подчинённое chartAt источникам.

LaTeX

$$$\\exists f: SmoothPartitionOfUnity, f.IsSubordinate chartAt_source$$$

Lean4

theorem exists_isSubordinate_chartAt_source :
    ∃ f : SmoothPartitionOfUnity M I M univ, f.IsSubordinate (fun x ↦ (chartAt H x).source) :=
  by
  apply exists_isSubordinate _ isClosed_univ _ (fun i ↦ (chartAt H _).open_source) (fun x _ ↦ ?_)
  exact mem_iUnion_of_mem x (mem_chart_source H x)

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