ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x x' : M<GOAL>((extChartAt I x').symm ≫ extChartAt I x).source = ↑I '' ((chartAt H x').symm ≫ₕ chartAt H x).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x x' : M<GOAL>ContDiffOn 𝕜 ⊤ (↑(extChartAt I x) ∘ ↑(extChartAt I x').symm) ((extChartAt I x').symm ≫ extChartAt I x).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x x' : M<VAR>y : E<VAR>hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source<GOAL>ContDiffWithinAt 𝕜 ⊤ (↑(extChartAt I x) ∘ ↑(extChartAt I x').symm) (Set.range ↑I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<VAR>y : E<VAR>h : y ∈ (extChartAt I x).target<GOAL>writtenInExtChartAt I I x (↑(chartAt H x)) y = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<VAR>y : E<VAR>h : y ∈ (extChartAt I x).target<GOAL>writtenInExtChartAt I I (↑(chartAt H x) x) (↑(chartAt H x).symm) y = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<VAR>y : E<VAR>h : y ∈ (extChartAt I x).target<GOAL>writtenInExtChartAt I 𝓘(𝕜, E) x (↑(extChartAt I x)) y = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<VAR>y : E<VAR>h : y ∈ (extChartAt I x).target<GOAL>writtenInExtChartAt 𝓘(𝕜, E) I (↑(extChartAt I x) x) (↑(extChartAt I x).symm) y = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : H<GOAL>↑(extChartAt I x) = ↑I
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x y : H<GOAL>↑(extChartAt I x) y = ↑I y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x y : E<GOAL>↑(extChartAt 𝓘(𝕜, E) x) y = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>ChartedSpace H M<VAR>ChartedSpace H' M'<VAR>x : M × M'<GOAL>extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>H : Type u_4<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>ChartedSpace H H'<VAR>x : M'<GOAL>extChartAt I x = (chartAt H' x).toPartialEquiv ≫ extChartAt I (↑(chartAt H' x) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>H : Type u_4<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>ChartedSpace H H'<VAR>x : M'<VAR>y : E<VAR>hy : y ∈ (extChartAt I x).target<GOAL>writtenInExtChartAt I I x (↑(chartAt H' x)) y = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>H : Type u_4<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>ChartedSpace H H'<VAR>x : M'<VAR>y : E<VAR>hy : y ∈ (extChartAt I x).target<GOAL>writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>LocallyCompactSpace 𝕜<VAR>FiniteDimensional 𝕜 E<GOAL>LocallyCompactSpace M
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothAdd I' G<VAR>f g : C^⊤⟮I, N; I', G⟯<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothMul I' G<VAR>f g : C^⊤⟮I, N; I', G⟯<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>E'' : Type u_7<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_8<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>N' : Type u_9<VAR>TopologicalSpace N'<VAR>ChartedSpace H'' N'<VAR>G : Type u_10<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothAdd I' G<VAR>f g : C^⊤⟮I'', N'; I', G⟯<VAR>h : C^⊤⟮I, N; I'', N'⟯<GOAL>(f + g).comp h = f.comp h + g.comp h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>E'' : Type u_7<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_8<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>N' : Type u_9<VAR>TopologicalSpace N'<VAR>ChartedSpace H'' N'<VAR>G : Type u_10<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothMul I' G<VAR>f g : C^⊤⟮I'', N'; I', G⟯<VAR>h : C^⊤⟮I, N; I'', N'⟯<GOAL>(f * g).comp h = f.comp h * g.comp h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>Zero G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<GOAL>⇑0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>One G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<GOAL>⇑1 = 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>Monoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothMul I' G<VAR>f : C^⊤⟮I, N; I', G⟯<VAR>n : ℕ<GOAL>⇑(f ^ n) = ⇑f ^ n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>AddMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothAdd I' G<VAR>f : C^⊤⟮I, N; I', G⟯<VAR>n : ℕ<GOAL>⇑(n • f) = n • ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>AddMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothAdd I' G<GOAL>∀ (a : C^⊤⟮I, N; I', G⟯) (a_1 : N), SmoothMap.coeFnAddMonoidHom a a_1 = a a_1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>Monoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>SmoothMul I' G<GOAL>∀ (a : C^⊤⟮I, N; I', G⟯) (a_1 : N), SmoothMap.coeFnMonoidHom a a_1 = a a_1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>LieAddGroup I' G<VAR>f : C^⊤⟮I, N; I', G⟯<GOAL>⇑(-f) = -⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>Group G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>LieGroup I' G<VAR>f : C^⊤⟮I, N; I', G⟯<GOAL>⇑f⁻¹ = (⇑f)⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>LieAddGroup I' G<VAR>f g : C^⊤⟮I, N; I', G⟯<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>G : Type u_10<VAR>Group G<VAR>TopologicalSpace G<VAR>ChartedSpace H' G<VAR>LieGroup I' G<VAR>f g : C^⊤⟮I, N; I', G⟯<GOAL>⇑(f / g) = ⇑f / ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>R : Type u_10<VAR>CommRing R<VAR>TopologicalSpace R<VAR>ChartedSpace H' R<VAR>SmoothRing I' R<GOAL>∀ (a : C^⊤⟮I, N; I', R⟯) (a_1 : N), SmoothMap.coeFnRingHom a a_1 = a a_1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>V : Type u_10<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>r : 𝕜<VAR>f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯<GOAL>⇑(r • f) = r • ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>E'' : Type u_7<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_8<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>N' : Type u_9<VAR>TopologicalSpace N'<VAR>ChartedSpace H'' N'<VAR>V : Type u_10<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>r : 𝕜<VAR>g : C^⊤⟮I'', N'; 𝓘(𝕜, V), V⟯<VAR>h : C^⊤⟮I, N; I'', N'⟯<GOAL>(r • g).comp h = r • g.comp h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>V : Type u_10<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<GOAL>∀ (a : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯) (a_1 : N), SmoothMap.coeFnLinearMap a a_1 = a a_1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>A : Type u_10<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>SmoothRing 𝓘(𝕜, A) A<GOAL>∀ (a : C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) (a_1 : N), SmoothMap.coeFnAlgHom a a_1 = a a_1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>N : Type u_6<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>E'' : Type u_7<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_8<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>N' : Type u_9<VAR>TopologicalSpace N'<VAR>ChartedSpace H'' N'<VAR>V : Type u_10<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : C^⊤⟮I'', N'; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>g : C^⊤⟮I'', N'; 𝓘(𝕜, V), V⟯<VAR>h : C^⊤⟮I, N; I'', N'⟯<GOAL>(f • g).comp h = f.comp h • g.comp h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>s : Set E<VAR>x : E<GOAL>HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s x f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>x : E<GOAL>HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) x f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>s : Set E<VAR>x : E<GOAL>MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>s : Set E<GOAL>MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>x : E<GOAL>MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<GOAL>MDifferentiable 𝓘(𝕜, E) 𝓘(𝕜, E') ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>x : E<GOAL>mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) x = f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>s : Set E<VAR>x : E<VAR>hs : UniqueMDiffWithinAt 𝓘(𝕜, E) s x<GOAL>mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s x = f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<VAR>s : Set E<VAR>x : E<GOAL>HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s x ↑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<VAR>x : E<GOAL>HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) x ↑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<VAR>s : Set E<VAR>x : E<GOAL>MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<VAR>s : Set E<GOAL>MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<VAR>x : E<GOAL>MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<GOAL>MDifferentiable 𝓘(𝕜, E) 𝓘(𝕜, E') ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<VAR>x : E<GOAL>mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) x = ↑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E ≃L[𝕜] E'<VAR>s : Set E<VAR>x : E<VAR>hs : UniqueMDiffWithinAt 𝓘(𝕜, E) s x<GOAL>mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f) s x = ↑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>x : M<GOAL>HasMFDerivWithinAt I I id s x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>MDifferentiableAt I I id x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>x : M<GOAL>MDifferentiableWithinAt I I id s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<GOAL>MDifferentiable I I id
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<GOAL>MDifferentiableOn I I id s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>x : M<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>mfderivWithin I I id s x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<GOAL>tangentMap I I id = id
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>p : TangentBundle I M<VAR>hs : UniqueMDiffWithinAt I s p.proj<GOAL>tangentMapWithin I I id s p = p