Hopf problem: uniformization · holomorphic cousin

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.HolomorphicCousin.exists_smoothPartitionOfUnity_eq_one_near_closed {ι : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] (U : ι → Set M) (hUo : ∀ (i : ι), IsOpen (U i)) (hUc : Set.univ ⊆ ⋃ (i : ι), U i) (i₀ : ι) {K : Set M} (hK : IsClosed K) (hKU : K ⊆ U i₀) : ∃ (V : Set M), IsOpen V ∧ K ⊆ V ∧ V ⊆ U i₀ ∧ ∃ (ρ : SmoothPartitionOfUnity ι I M), ρ.IsSubordinate U ∧ (∀ x ∈ V, (ρ i₀) x = 1) ∧ (∀ (i : ι), i ≠ i₀ → ∀ x ∈ V, (ρ i) x = 0) ∧ ∀ (i : ι), i ≠ i₀ → Disjoint (tsupport ⇑(ρ i)) V