theorem SmoothPartitionOfUnity.sum_germ {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) {x : M} (hx : x ∈ interior s := by simp) : ∑ i ∈ ρ.fintsupport x, ⟨↑⇑(ρ i), ⋯⟩ = 1

noncomputable def SmoothPartitionOfUnity.combine {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [AddCommGroup F] [Module ℝ F] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (φ : ι → M → F) (x : M) : F

Equations

• ρ.combine φ x = ∑ᶠ (i : ι), (ρ i) x • φ i x

theorem SmoothPartitionOfUnity.germ_combine_mem {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [AddCommGroup F] [Module ℝ F] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) {x : M} (φ : ι → M → F) (hx : x ∈ interior s := by simp) : ↑(ρ.combine φ) ∈ reallyConvexHull (↥(smoothGerm I x)) ((fun (i : ι) => ↑(φ i)) '' ↑(ρ.fintsupport x))