ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>SubNegMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<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>f : M → G<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiff I' I n f<GOAL>ContMDiff I' I n fun x => f x - c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>DivInvMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<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>f : M → G<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiff I' I n f<GOAL>ContMDiff I' I n fun x => f x / c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>DivInvMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<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>f : M → G<VAR>s : Set M<VAR>x : M<VAR>c : G<VAR>hf : SmoothWithinAt I' I f s x<GOAL>SmoothWithinAt I' I (fun x => f x / c) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>SubNegMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<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>f : M → G<VAR>s : Set M<VAR>x : M<VAR>c : G<VAR>hf : SmoothWithinAt I' I f s x<GOAL>SmoothWithinAt I' I (fun x => f x - c) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>DivInvMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<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>f : M → G<VAR>x : M<VAR>c : G<VAR>hf : SmoothAt I' I f x<GOAL>SmoothAt I' I (fun x => f x / c) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>SubNegMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<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>f : M → G<VAR>x : M<VAR>c : G<VAR>hf : SmoothAt I' I f x<GOAL>SmoothAt I' I (fun x => f x - c) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>DivInvMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<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>f : M → G<VAR>s : Set M<VAR>c : G<VAR>hf : SmoothOn I' I f s<GOAL>SmoothOn I' I (fun x => f x / c) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>SubNegMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<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>f : M → G<VAR>s : Set M<VAR>c : G<VAR>hf : SmoothOn I' I f s<GOAL>SmoothOn I' I (fun x => f x - c) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>SubNegMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<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>f : M → G<VAR>c : G<VAR>hf : Smooth I' I f<GOAL>Smooth I' I fun x => f x - c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>DivInvMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<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>f : M → G<VAR>c : G<VAR>hf : Smooth I' I f<GOAL>Smooth I' I fun x => f x / c
<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>c : M<VAR>self : SmoothBumpFunction I c<GOAL>Metric.closedBall (↑(extChartAt I c) c) self.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>↑f = (chartAt H c).source.indicator (↑f.toContDiffBump ∘ ↑(extChartAt I c))
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>0 < f.rOut
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I = Metric.ball (↑(extChartAt I c) c) f.rOut ∩ (extChartAt I c).target
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>Set.EqOn (↑f) (↑f.toContDiffBump ∘ ↑(extChartAt I c)) (chartAt H c).source
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>hx : x ∈ (chartAt H c).source<GOAL>↑f =ᶠ[𝓝 x] ↑f.toContDiffBump ∘ ↑(extChartAt I c)
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>hs : x ∈ (chartAt H c).source<VAR>hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) ≤ f.rIn<GOAL>↑f x = 1
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>Function.support ↑f = (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' Metric.ball (↑(extChartAt I c) c) f.rOut
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>IsOpen (Function.support ↑f)
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>Function.support ↑f = ↑(extChartAt I c).symm '' (Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>Function.support ↑f ⊆ (chartAt H c).source
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>s : Set M<VAR>hs : s ⊆ Function.support ↑f<GOAL>↑(extChartAt I c) '' s = Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>↑f x ∈ Set.Icc 0 1
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>0 ≤ ↑f x
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>↑f x ≤ 1
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>hs : x ∈ (chartAt H c).source<VAR>hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn<GOAL>↑f =ᶠ[𝓝 x] 1
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>↑f =ᶠ[𝓝 c] 1
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>↑f c = 1
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>Function.support ↑f ∈ 𝓝 c
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>tsupport ↑f ∈ 𝓝 c
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>c ∈ Function.support ↑f
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>(Function.support ↑f).Nonempty
<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>c : M<VAR>f : SmoothBumpFunction I c<GOAL>IsCompact (↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I))
<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>c : M<GOAL>(𝓝[Set.range ↑I] ↑(extChartAt I c) c).HasBasis (fun x => True) fun f => Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑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>c : M<VAR>f : SmoothBumpFunction I c<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ Function.support ↑f<GOAL>IsClosed (↑(extChartAt I c) '' s)
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ Function.support ↑f<GOAL>∃ r ∈ Set.Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' Metric.ball (↑(extChartAt I c) c) r
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>r : ℝ<VAR>hr : r ∈ Set.Ioo 0 f.rOut<GOAL>(f.updateRIn r hr).rOut = f.rOut
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>r : ℝ<VAR>hr : r ∈ Set.Ioo 0 f.rOut<GOAL>(f.updateRIn r hr).rIn = r
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>r : ℝ<VAR>hr : r ∈ Set.Ioo 0 f.rOut<GOAL>Function.support ↑(f.updateRIn r hr) = Function.support ↑f
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<GOAL>IsClosed (↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<GOAL>tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<GOAL>tsupport ↑f ⊆ (extChartAt I c).source
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<GOAL>tsupport ↑f ⊆ (chartAt H c).source
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<GOAL>HasCompactSupport ↑f
<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>c : M<VAR>T2Space M<GOAL>(𝓝 c).HasBasis (fun x => True) fun f => tsupport ↑f
<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>c : M<VAR>T2Space M<VAR>s : Set M<VAR>hs : s ∈ 𝓝 c<GOAL>(𝓝 c).HasBasis (fun f => tsupport ↑f ⊆ s) fun f => Function.support ↑f
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<VAR>SmoothManifoldWithCorners I M<GOAL>Smooth I 𝓘(ℝ, ℝ) ↑f
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>SmoothAt I 𝓘(ℝ, ℝ) (↑f) x
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<VAR>SmoothManifoldWithCorners I M<GOAL>Continuous ↑f
<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>c : M<VAR>f : SmoothBumpFunction I c<VAR>T2Space M<VAR>SmoothManifoldWithCorners I M<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>g : M → G<VAR>hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).source<GOAL>Smooth I 𝓘(ℝ, G) fun x => ↑f x • g 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>self : ModelWithCorners 𝕜 E H<GOAL>self.source = Set.univ
<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>self : ModelWithCorners 𝕜 E H<GOAL>UniqueDiffOn 𝕜 self.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>self : ModelWithCorners 𝕜 E H<GOAL>Continuous ↑self.toPartialEquiv
<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>self : ModelWithCorners 𝕜 E H<GOAL>Continuous self.invFun
<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<GOAL>↑I.toPartialEquiv = ↑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>e : PartialEquiv H E<VAR>a : e.source = Set.univ<VAR>b : UniqueDiffOn 𝕜 e.target<VAR>c : Continuous ↑e<VAR>d : Continuous e.invFun<GOAL>↑{ toPartialEquiv := e, source_eq := a, unique_diff' := b, continuous_toFun := c, continuous_invFun := d } = ↑e
<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<GOAL>↑I.symm = ↑I.symm
<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>e : PartialEquiv H E<VAR>a : e.source = Set.univ<VAR>b : UniqueDiffOn 𝕜 e.target<VAR>c : Continuous ↑e<VAR>d : Continuous e.invFun<GOAL>{ toPartialEquiv := e, source_eq := a, unique_diff' := b, continuous_toFun := c, continuous_invFun := d }.symm = e.symm
<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<GOAL>Continuous ↑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>x : H<GOAL>ContinuousAt (↑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>s : Set H<VAR>x : H<GOAL>ContinuousWithinAt (↑I) 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<GOAL>Continuous ↑I.symm
<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>x : E<GOAL>ContinuousAt (↑I.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>s : Set E<VAR>x : E<GOAL>ContinuousWithinAt (↑I.symm) 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>s : Set E<GOAL>ContinuousOn (↑I.symm) 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<GOAL>I.target = 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<GOAL>UniqueDiffOn 𝕜 (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>x : H<GOAL>↑I.symm (↑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<GOAL>Function.LeftInverse ↑I.symm ↑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<GOAL>Function.Injective ↑I