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>SmoothManifoldWithCorners I M<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>MDifferentiableAt I I (↑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>h : e ∈ atlas H M<GOAL>MDifferentiableOn I I (↑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>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<GOAL>MDifferentiableAt I I (↑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>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<GOAL>MDifferentiableOn I I (↑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>h : e ∈ atlas H M<GOAL>PartialHomeomorph.MDifferentiable I I 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<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>PartialHomeomorph.MDifferentiable I I (chartAt H 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>p q : TangentBundle I M<VAR>h : q.proj ∈ (chartAt H p.proj).source<GOAL>tangentMap I I (↑(chartAt H p.proj)) q = (Bundle.TotalSpace.toProd H E).symm (↑(chartAt (ModelProd H E) p) q)
<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>p : TangentBundle I M<VAR>q : TangentBundle I H<VAR>h : q.proj ∈ (chartAt H p.proj).target<GOAL>tangentMap I I (↑(chartAt H p.proj).symm) q = ↑(chartAt (ModelProd H E) p).symm ((Bundle.TotalSpace.toProd H E) q)
<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 y : M<VAR>hsrc : x ∈ (chartAt H y).source<GOAL>mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y 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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<GOAL>PartialHomeomorph.MDifferentiable I' I 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<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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>MDifferentiableAt I I' (↑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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>x : M'<VAR>hx : x ∈ e.target<GOAL>MDifferentiableAt I' I (↑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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>(mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) 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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M'<VAR>hx : x ∈ e.target<GOAL>(mfderiv I I' (↑e) (↑e.symm x)).comp (mfderiv I' I (↑e.symm) 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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>Function.Bijective ⇑(mfderiv I I' (↑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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>Function.Injective ⇑(mfderiv I I' (↑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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>Function.Surjective ⇑(mfderiv I I' (↑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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>LinearMap.ker (mfderiv I I' (↑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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>LinearMap.range (mfderiv I I' (↑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>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 : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>Set.range ⇑(mfderiv I I' (↑e) x) = 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>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>e : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners I' M'<VAR>SmoothManifoldWithCorners I'' M''<VAR>he' : PartialHomeomorph.MDifferentiable I' I'' e'<GOAL>PartialHomeomorph.MDifferentiable I I'' (e ≫ₕ e')
<VAR>𝕜 : Type u_11<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_12<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_13<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_14<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x y : M<VAR>h : y ∈ (chartAt H x).source<GOAL>HasMFDerivAt I 𝓘(𝕜, E) (↑(extChartAt I x)) y (mfderiv I I (↑(chartAt H x)) y)
<VAR>𝕜 : Type u_11<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_12<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_13<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_14<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>x y : M<VAR>h : y ∈ (chartAt H x).source<GOAL>HasMFDerivWithinAt I 𝓘(𝕜, E) (↑(extChartAt I x)) s y (mfderiv I I (↑(chartAt H x)) y)
<VAR>𝕜 : Type u_11<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_12<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_13<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_14<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x y : M<VAR>h : y ∈ (chartAt H x).source<GOAL>MDifferentiableAt I 𝓘(𝕜, E) (↑(extChartAt I x)) y
<VAR>𝕜 : Type u_11<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_12<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_13<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_14<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>MDifferentiableOn I 𝓘(𝕜, E) (↑(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>s : Set H<VAR>hs : IsOpen s<GOAL>PartialHomeomorph.ofSet s hs ∈ analyticGroupoid 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>e : PartialHomeomorph M H<GOAL>e.symm ≫ₕ e ∈ analyticGroupoid 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>CompleteSpace E<VAR>I.Boundaryless<VAR>e : PartialHomeomorph H H<GOAL>e ∈ analyticGroupoid I ↔ AnalyticOn 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I '' e.source) ∧ AnalyticOn 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I '' e.target)
<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>R : Type u_4<VAR>Semiring R<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>self : SmoothRing I R<GOAL>Smooth (I.prod I) I fun p => p.1 * p.2
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>TopologicalSpace R<VAR>TopologicalSpace H<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ChartedSpace H R<VAR>I : ModelWithCorners 𝕜 E H<VAR>Semiring R<VAR>SmoothRing I R<GOAL>TopologicalSemiring R
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>Group α<VAR>self : UniformGroup α<GOAL>UniformContinuous fun p => p.1 / p.2
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>self : UniformAddGroup α<GOAL>UniformContinuous fun p => p.1 - p.2
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>Group α<VAR>h₁ : UniformContinuous fun p => p.1 * p.2<VAR>h₂ : UniformContinuous fun p => p⁻¹<GOAL>UniformGroup α
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>h₁ : UniformContinuous fun p => p.1 + p.2<VAR>h₂ : UniformContinuous fun p => -p<GOAL>UniformAddGroup α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<GOAL>UniformContinuous fun p => p.1 / p.2
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>UniformContinuous fun p => p.1 - p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun x => f x / g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun x => f x - g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<GOAL>UniformContinuous fun x => (f x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<GOAL>UniformContinuous fun x => -f x
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<GOAL>UniformContinuous fun x => x⁻¹
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>UniformContinuous fun x => -x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun x => f x * g x
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>UniformContinuous fun p => p.1 + p.2
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<GOAL>UniformContinuous fun p => p.1 * p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => n • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => f x ^ n
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>n : ℕ<GOAL>UniformContinuous fun x => n • x
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>n : ℕ<GOAL>UniformContinuous fun x => x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℤ<GOAL>UniformContinuous fun x => n • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℤ<GOAL>UniformContinuous fun x => f x ^ n
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>n : ℤ<GOAL>UniformContinuous fun x => x ^ n
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>n : ℤ<GOAL>UniformContinuous fun x => n • x
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>a : α<GOAL>Filter.map (fun x => (x.1 + a, x.2 + a)) (𝓤 α) = 𝓤 α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>a : α<GOAL>Filter.map (fun x => (x.1 * a, x.2 * a)) (𝓤 α) = 𝓤 α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>a : α<GOAL>UniformEmbedding fun x => x + a
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>a : α<GOAL>UniformEmbedding fun x => x * a
<VAR>β : Type u_2<VAR>AddGroup β<VAR>us : Set (UniformSpace β)<VAR>h : ∀ u ∈ us, UniformAddGroup β<GOAL>UniformAddGroup β
<VAR>β : Type u_2<VAR>Group β<VAR>us : Set (UniformSpace β)<VAR>h : ∀ u ∈ us, UniformGroup β<GOAL>UniformGroup β
<VAR>β : Type u_2<VAR>Group β<VAR>ι : Sort u_3<VAR>us' : ι → UniformSpace β<VAR>h' : ∀ (i : ι), UniformGroup β<GOAL>UniformGroup β
<VAR>β : Type u_2<VAR>AddGroup β<VAR>ι : Sort u_3<VAR>us' : ι → UniformSpace β<VAR>h' : ∀ (i : ι), UniformAddGroup β<GOAL>UniformAddGroup β
<VAR>β : Type u_2<VAR>Group β<VAR>u₁ u₂ : UniformSpace β<VAR>h₁ : UniformGroup β<VAR>h₂ : UniformGroup β<GOAL>UniformGroup β
<VAR>β : Type u_2<VAR>AddGroup β<VAR>u₁ u₂ : UniformSpace β<VAR>h₁ : UniformAddGroup β<VAR>h₂ : UniformAddGroup β<GOAL>UniformAddGroup β
<VAR>β : Type u_2<VAR>AddGroup β<VAR>γ : Type u_3<VAR>AddGroup γ<VAR>UniformSpace γ<VAR>UniformAddGroup γ<VAR>UniformSpace β<VAR>F : Type u_4<VAR>FunLike F β γ<VAR>AddMonoidHomClass F β γ<VAR>f : F<VAR>hf : UniformInducing ⇑f<GOAL>UniformAddGroup β
<VAR>β : Type u_2<VAR>Group β<VAR>γ : Type u_3<VAR>Group γ<VAR>UniformSpace γ<VAR>UniformGroup γ<VAR>UniformSpace β<VAR>F : Type u_4<VAR>FunLike F β γ<VAR>MonoidHomClass F β γ<VAR>f : F<VAR>hf : UniformInducing ⇑f<GOAL>UniformGroup β
<VAR>β : Type u_2<VAR>Group β<VAR>γ : Type u_3<VAR>Group γ<VAR>u : UniformSpace γ<VAR>UniformGroup γ<VAR>F : Type u_4<VAR>FunLike F β γ<VAR>MonoidHomClass F β γ<VAR>f : F<GOAL>UniformGroup β
<VAR>β : Type u_2<VAR>AddGroup β<VAR>γ : Type u_3<VAR>AddGroup γ<VAR>u : UniformSpace γ<VAR>UniformAddGroup γ<VAR>F : Type u_4<VAR>FunLike F β γ<VAR>AddMonoidHomClass F β γ<VAR>f : F<GOAL>UniformAddGroup β
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>𝓤 α = Filter.comap (fun x => x.2 - x.1) (𝓝 0)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<GOAL>𝓤 α = Filter.comap (fun x => x.2 / x.1) (𝓝 1)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<GOAL>𝓤 α = Filter.comap (fun x => x.1 / x.2) (𝓝 1)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>𝓤 α = Filter.comap (fun x => x.1 - x.2) (𝓝 0)
<VAR>G : Type u_3<VAR>Group G<VAR>u v : UniformSpace G<VAR>hu : UniformGroup G<VAR>hv : UniformGroup G<VAR>h : 𝓝 1 = 𝓝 1<GOAL>u = v
<VAR>G : Type u_3<VAR>AddGroup G<VAR>u v : UniformSpace G<VAR>hu : UniformAddGroup G<VAR>hv : UniformAddGroup G<VAR>h : 𝓝 0 = 𝓝 0<GOAL>u = v
<VAR>G : Type u_3<VAR>AddGroup G<VAR>u v : UniformSpace G<VAR>hu : UniformAddGroup G<VAR>hv : UniformAddGroup G<GOAL>u = v ↔ 𝓝 0 = 𝓝 0
<VAR>G : Type u_3<VAR>Group G<VAR>u v : UniformSpace G<VAR>hu : UniformGroup G<VAR>hv : UniformGroup G<GOAL>u = v ↔ 𝓝 1 = 𝓝 1
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>(𝓝 0).IsCountablyGenerated<GOAL>(𝓤 α).IsCountablyGenerated
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>(𝓝 1).IsCountablyGenerated<GOAL>(𝓤 α).IsCountablyGenerated
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<GOAL>𝓤 α = Filter.comap (fun x => x.1⁻¹ * x.2) (𝓝 1)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>𝓤 α = Filter.comap (fun x => -x.1 + x.2) (𝓝 0)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>𝓤 α = Filter.comap (fun x => -x.2 + x.1) (𝓝 0)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<GOAL>𝓤 α = Filter.comap (fun x => x.2⁻¹ * x.1) (𝓝 1)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 0).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.2 - x.1 ∈ U i}
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.2 / x.1 ∈ U i}
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.1⁻¹ * x.2 ∈ U i}
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 0).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | -x.1 + x.2 ∈ U i}
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.1 / x.2 ∈ U i}
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 0).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.1 - x.2 ∈ U i}
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 0).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | -x.2 + x.1 ∈ U i}
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.2⁻¹ * x.1 ∈ U i}