ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>mfderivWithin I I'' (g ∘ f) s x = (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f 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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>x : M<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>hg : MDifferentiableAt I' I'' g (f x)<VAR>hf : MDifferentiableAt I I' f x<GOAL>mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f 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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>y : M'<VAR>hg : MDifferentiableAt I' I'' g y<VAR>hf : MDifferentiableAt I I' f x<VAR>hy : f x = y<GOAL>mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f 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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>hg : MDifferentiableOn I' I'' g u<VAR>hf : MDifferentiableOn I I' f s<VAR>st : s ⊆ f ⁻¹' u<GOAL>MDifferentiableOn I I'' (g ∘ f) 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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>hg : MDifferentiable I' I'' g<VAR>hf : MDifferentiable I I' f<GOAL>MDifferentiable I I'' (g ∘ 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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>p : TangentBundle I M<VAR>hg : MDifferentiableWithinAt I' I'' g u (f p.proj)<VAR>hf : MDifferentiableWithinAt I I' f s p.proj<VAR>h : s ⊆ f ⁻¹' u<VAR>hps : UniqueMDiffWithinAt I s p.proj<GOAL>tangentMapWithin I I'' (g ∘ f) s p = tangentMapWithin I' I'' g u (tangentMapWithin I I' f s p)
<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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>p : TangentBundle I M<VAR>hg : MDifferentiableAt I' I'' g (f p.proj)<VAR>hf : MDifferentiableAt I I' f p.proj<GOAL>tangentMap I I'' (g ∘ f) p = tangentMap I' I'' g (tangentMap I I' f p)
<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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>hg : MDifferentiable I' I'' g<VAR>hf : MDifferentiable I I' f<GOAL>tangentMap I I'' (g ∘ f) = tangentMap I' I'' g ∘ tangentMap I I' f
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f' : E →L[ℝ] F<VAR>h : IsConformalMap f'<VAR>u v : E<GOAL>InnerProductGeometry.angle (f' u) (f' v) = InnerProductGeometry.angle u v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<VAR>f' : E →L[ℝ] F<VAR>h : HasFDerivAt f f' x<VAR>H : ConformalAt f x<VAR>u v : E<GOAL>InnerProductGeometry.angle (f' u) (f' v) = InnerProductGeometry.angle u v
<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>n : ℕ∞<GOAL>ContMDiff I 𝓘(𝕜, E) n ↑I
<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>n : ℕ∞<GOAL>ContMDiffOn 𝓘(𝕜, E) I n (↑I.symm) (Set.range ↑I)
<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>e : PartialHomeomorph M H<VAR>n : ℕ∞<VAR>h : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<GOAL>ContMDiffOn I I n (↑e) e.source
<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>e : PartialHomeomorph M H<VAR>n : ℕ∞<VAR>h : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<GOAL>ContMDiffOn I I n (↑e.symm) e.target
<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>e : PartialHomeomorph M H<VAR>x : M<VAR>n : ℕ∞<VAR>h : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>hx : x ∈ e.source<GOAL>ContMDiffAt I I n (↑e) 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>e : PartialHomeomorph M H<VAR>n : ℕ∞<VAR>x : H<VAR>h : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>hx : x ∈ e.target<GOAL>ContMDiffAt I I n (↑e.symm) 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<VAR>n : ℕ∞<GOAL>ContMDiffOn I I n (↑(chartAt H x)) (chartAt H x).source
<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<VAR>n : ℕ∞<GOAL>ContMDiffOn I I n (↑(chartAt H x).symm) (chartAt H x).target
<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>e : PartialHomeomorph M H<VAR>n : ℕ∞<VAR>x : M<VAR>he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>hx : x ∈ e.source<GOAL>ContMDiffAt I 𝓘(𝕜, E) n (↑(e.extend 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<VAR>n : ℕ∞<VAR>x' : M<VAR>h : x' ∈ (chartAt H x).source<GOAL>ContMDiffAt I 𝓘(𝕜, E) n (↑(extChartAt I x)) 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<VAR>n : ℕ∞<GOAL>ContMDiffAt I 𝓘(𝕜, E) n (↑(extChartAt I x)) 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<VAR>n : ℕ∞<GOAL>ContMDiffOn I 𝓘(𝕜, E) n (↑(extChartAt I x)) (chartAt H x).source
<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>e : PartialHomeomorph M H<VAR>n : ℕ∞<VAR>he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<GOAL>ContMDiffOn 𝓘(𝕜, E) I n (↑(e.extend I).symm) (↑I '' e.target)
<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>n : ℕ∞<VAR>x : M<GOAL>ContMDiffOn 𝓘(𝕜, E) I n (↑(extChartAt I x).symm) (extChartAt I x).target
<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>n : ℕ∞<VAR>e' : PartialHomeomorph H H<VAR>h : e' ∈ contDiffGroupoid ⊤ I<GOAL>ContMDiffOn I I n (↑e') e'.source
<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>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : ChartedSpace.LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<GOAL>SmoothOn I I (↑f) f.source
<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>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<GOAL>ChartedSpace.LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source ↔ SmoothOn I I (↑f) f.source ∧ SmoothOn I I (↑f.symm) f.target
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑↑Y<VAR>x : ↥((TopologicalSpace.Opens.map α.base).obj U)<GOAL>Y.presheaf.germ ⟨α.base ↑x, ⋯⟩ ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α ↑x = α.c.app (Opposite.op U) ≫ X.presheaf.germ x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑↑Y<VAR>x : ↑↑X<VAR>hx : α.base x ∈ U<GOAL>Y.presheaf.germ ⟨α.base x, hx⟩ ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x = α.c.app (Opposite.op U) ≫ X.presheaf.germ ⟨x, hx⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>V : TopologicalSpace.Opens ↑U<VAR>x : ↑U<VAR>hx : x ∈ V<GOAL>(X.restrict h).presheaf.germ ⟨x, hx⟩ ≫ (X.restrictStalkIso h x).hom = X.presheaf.germ ⟨f x, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>V : TopologicalSpace.Opens ↑U<VAR>x : ↑U<VAR>hx : x ∈ V<GOAL>X.presheaf.germ ⟨f x, ⋯⟩ ≫ (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ ⟨x, hx⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<GOAL>(X.restrictStalkIso h x).inv = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.ofRestrict h) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>x : ↑↑X<GOAL>AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>α : X ⟶ Y<VAR>β : Y ⟶ Z<VAR>x : ↑↑X<GOAL>AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (α ≫ β) x = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap β (α.base x) ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α β : X ⟶ Y<VAR>h₁ : α = β<VAR>x x' : ↑↑X<VAR>h₂ : x = x'<GOAL>AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x ≫ CategoryTheory.eqToHom ⋯ = CategoryTheory.eqToHom ⋯ ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap β x'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α β : X ⟶ Y<VAR>h : α = β<VAR>x : ↑↑X<GOAL>AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x = CategoryTheory.eqToHom ⋯ ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap β x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α : X ⟶ Y<VAR>x x' : ↑↑X<VAR>h : x = x'<GOAL>AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x ≫ CategoryTheory.eqToHom ⋯ = CategoryTheory.eqToHom ⋯ ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>x y : ↑↑X<VAR>h : x ⤳ y<GOAL>Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y ≫ X.presheaf.stalkSpecializes h
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>h : IsIntegralCurve γ v<VAR>s : Set ℝ<GOAL>IsIntegralCurveOn γ v s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<GOAL>IsIntegralCurve γ v ↔ IsIntegralCurveOn γ v Set.univ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<GOAL>IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<GOAL>IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>h : IsIntegralCurve γ v<VAR>t : ℝ<GOAL>IsIntegralCurveAt γ v t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<GOAL>IsIntegralCurve γ v ↔ ∀ (t : ℝ), IsIntegralCurveAt γ v t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>h : IsIntegralCurveOn γ v s<VAR>hs : s' ⊆ s<GOAL>IsIntegralCurveOn γ v s'
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>h : IsIntegralCurveOn γ v s<VAR>h' : IsIntegralCurveOn γ v s'<GOAL>IsIntegralCurveOn γ v (s ∪ s')
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>h : IsIntegralCurveAt γ v t₀<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I γ t₀ (ContinuousLinearMap.smulRight 1 (v (γ t₀)))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>t₀ : ℝ<VAR>h : IsIntegralCurveOn γ v s<VAR>hs : s ∈ 𝓝 t₀<GOAL>IsIntegralCurveAt γ v t₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>h : ∀ t ∈ s, IsIntegralCurveAt γ v t<GOAL>IsIntegralCurveOn γ v s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>hs : IsOpen s<GOAL>IsIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsIntegralCurveAt γ v t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>ht : t₀ ∈ s<GOAL>ContinuousAt γ t₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>hγ : IsIntegralCurveOn γ v s<GOAL>ContinuousOn γ s