ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>he : ∀ (x : M), f x ∈ e.source<GOAL>Smooth IM (IB.prod 𝓘(𝕜, F)) f ↔ (Smooth IM IB fun x => (f x).proj) ∧ Smooth IM 𝓘(𝕜, F) fun x => (↑e (f x)).2
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<GOAL>SmoothOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) (↑e) e.source
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<GOAL>SmoothOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) (↑e.symm) e.target
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_11<VAR>Z : VectorBundleCore 𝕜 B F ι<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>self : Z.IsSmooth IB<VAR>i j : ι<GOAL>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_11<VAR>Z : VectorBundleCore 𝕜 B F ι<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>h : Z.IsSmooth IB<VAR>i j : ι<GOAL>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>self : VectorPrebundle.IsSmooth IB a<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<GOAL>e ∈ a.pretrivializationAtlas → ∀ e' ∈ a.pretrivializationAtlas, ∃ f, SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) f (e.baseSet ∩ e'.baseSet) ∧ ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' { proj := b, snd := e.symm b v }).2
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : VectorPrebundle.IsSmooth IB a<VAR>e e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<VAR>he' : e' ∈ a.pretrivializationAtlas<GOAL>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (VectorPrebundle.smoothCoordChange IB a he he') (e.baseSet ∩ e'.baseSet)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : VectorPrebundle.IsSmooth IB a<VAR>e e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<VAR>he' : e' ∈ a.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>(VectorPrebundle.smoothCoordChange IB a he he' b) v = (↑e' { proj := b, snd := e.symm b v }).2
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : VectorPrebundle.IsSmooth IB a<VAR>e e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<VAR>he' : e' ∈ a.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>(b, (VectorPrebundle.smoothCoordChange IB a he he' b) v) = ↑e' { proj := b, snd := e.symm b v }
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : VectorPrebundle.IsSmooth IB a<GOAL>SmoothVectorBundle F E IB
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : optParam (Set M) Set.univ<VAR>self : SmoothBumpCovering ι I M s<VAR>x : M<GOAL>x ∈ s → ∃ i, ↑(self.toFun i) =ᶠ[𝓝 x] 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : optParam (Set M) Set.univ<VAR>self : SmoothBumpCovering ι I M s<VAR>i : ι<GOAL>self.c i ∈ s
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : optParam (Set M) Set.univ<VAR>self : SmoothBumpCovering ι I M s<GOAL>LocallyFinite fun i => Function.support ↑(self.toFun i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : optParam (Set M) Set.univ<VAR>self : SmoothPartitionOfUnity ι I M s<VAR>x : M<GOAL>∑ᶠ (i : ι), (self.toFun i) x ≤ 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : optParam (Set M) Set.univ<VAR>self : SmoothPartitionOfUnity ι I M s<VAR>x : M<GOAL>x ∈ s → ∑ᶠ (i : ι), (self.toFun i) x = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : optParam (Set M) Set.univ<VAR>self : SmoothPartitionOfUnity ι I M s<GOAL>LocallyFinite fun i => Function.support ⇑(self.toFun i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : optParam (Set M) Set.univ<VAR>self : SmoothPartitionOfUnity ι I M s<VAR>i : ι<VAR>x : M<GOAL>0 ≤ (self.toFun i) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<GOAL>LocallyFinite fun i => Function.support ⇑(f i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>i : ι<VAR>x : M<GOAL>0 ≤ (f i) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>∑ᶠ (i : ι), (f i) x = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>∃ i, 0 < (f i) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>x : M<GOAL>∑ᶠ (i : ι), (f i) x ≤ 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>i : ι<GOAL>f.toPartitionOfUnity i = ↑(f i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<GOAL>Smooth I 𝓘(ℝ, ℝ) fun x => ∑ᶠ (i : ι), (f i) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>i : ι<VAR>x : M<GOAL>(f i) x ≤ 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>x : M<GOAL>0 ≤ ∑ᶠ (i : ι), (f i) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>g : M → F<VAR>i : ι<VAR>hg : ∀ x ∈ tsupport ⇑(f i), ContMDiffAt I 𝓘(ℝ, F) n g x<GOAL>ContMDiff I 𝓘(ℝ, F) n fun x => (f i) x • g x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>g : M → F<VAR>i : ι<VAR>hg : ∀ x ∈ tsupport ⇑(f i), SmoothAt I 𝓘(ℝ, F) g x<GOAL>Smooth I 𝓘(ℝ, F) fun x => (f i) x • g x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>g : ι → M → F<VAR>hg : ∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), ContMDiffAt I 𝓘(ℝ, F) n (g i) x<GOAL>ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ (i : ι), (f i) x • g i x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>g : ι → M → F<VAR>hg : ∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), SmoothAt I 𝓘(ℝ, F) (g i) x<GOAL>Smooth I 𝓘(ℝ, F) fun x => ∑ᶠ (i : ι), (f i) x • g i x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>x₀ : M<VAR>g : ι → M → F<VAR>hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) n (g i) x₀<GOAL>ContMDiffAt I 𝓘(ℝ, F) n (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s<VAR>x₀ : E<VAR>g : ι → E → F<VAR>hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContDiffAt ℝ n (g i) x₀<GOAL>ContDiffAt ℝ n (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>g : ι → M → F<VAR>t : Set F<VAR>x : M<VAR>hx : x ∈ s<VAR>hg : ∀ (i : ι), (f i) x ≠ 0 → g i x ∈ t<VAR>ht : Convex ℝ t<GOAL>∑ᶠ (i : ι), (f i) x • g i x ∈ t
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<VAR>i : ι<GOAL>i ∈ ρ.finsupport x₀ ↔ i ∈ Function.support fun i => (ρ i) x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<GOAL>↑(ρ.finsupport x₀) = Function.support fun i => (ρ i) x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<VAR>hx₀ : x₀ ∈ s<GOAL>∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<VAR>hx₀ : x₀ ∈ s<GOAL>∀ {I_1 : Finset ι}, ρ.finsupport x₀ ⊆ I_1 → ∑ i ∈ I_1, (ρ i) x₀ = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>Module ℝ A<VAR>φ : ι → M → A<GOAL>∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ • φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ • φ i x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<GOAL>{i | x₀ ∈ tsupport ⇑(ρ i)}.Finite
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<VAR>i : ι<GOAL>i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport ⇑(ρ i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<GOAL>∀ᶠ (y : M) in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<GOAL>ρ.finsupport x₀ ⊆ ρ.fintsupport x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ρ : SmoothPartitionOfUnity ι I M s<VAR>x₀ : M<GOAL>∀ᶠ (y : M) in 𝓝 x₀, ρ.finsupport y ⊆ ρ.fintsupport x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>U : ι → Set M<GOAL>f.toPartitionOfUnity.IsSubordinate U ↔ f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>U : ι → Set M<VAR>g : ι → M → F<VAR>hf : f.IsSubordinate U<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hg : ∀ (i : ι), ContMDiffOn I 𝓘(ℝ, F) n (g i) (U i)<GOAL>ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ (i : ι), (f i) x • g i x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>U : ι → Set M<VAR>g : ι → M → F<VAR>hf : f.IsSubordinate U<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hg : ∀ (i : ι), SmoothOn I 𝓘(ℝ, F) (g i) (U i)<GOAL>Smooth I 𝓘(ℝ, F) fun x => ∑ᶠ (i : ι), (f i) x • g i x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : BumpCovering ι M s<VAR>hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ⇑(f i)<VAR>i : ι<GOAL>Smooth I 𝓘(ℝ, ℝ) ⇑(f.toPartitionOfUnity i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : BumpCovering ι M s<VAR>hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ⇑(f i)<GOAL>(f.toSmoothPartitionOfUnity hf).toPartitionOfUnity = f.toPartitionOfUnity
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : BumpCovering ι M s<VAR>hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ⇑(f i)<VAR>i : ι<GOAL>⇑((f.toSmoothPartitionOfUnity hf) i) = ⇑(f.toPartitionOfUnity i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>f : BumpCovering ι M s<VAR>U : ι → Set M<VAR>h : f.IsSubordinate U<VAR>hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ⇑(f i)<GOAL>(f.toSmoothPartitionOfUnity hf).IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>U : M → Set M<VAR>h : fs.IsSubordinate U<VAR>i : ι<GOAL>Function.support ↑(fs.toFun i) ⊆ U (fs.c i)
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>U : M → Set M<VAR>T2Space M<VAR>SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<GOAL>LocallyFinite fun i => Function.support ↑(fs.toFun i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>x : M<GOAL>{i | ↑(fs.toFun i) x ≠ 0}.Finite
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>i : ι<VAR>x : M<VAR>h : ↑(fs.toFun i) x = 1<GOAL>x ∈ (chartAt H (fs.c i)).source
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>i : ι<VAR>x : M<VAR>h : ↑(fs.toFun i) x = 1<GOAL>x ∈ (extChartAt I (fs.c i)).source
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>↑(fs.toFun (fs.ind x hx)) =ᶠ[𝓝 x] 1