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>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : N → M'<VAR>s : Set M<VAR>x : M<VAR>hm : m ≤ n<GOAL>ContMDiffWithinAt I I' m (f ∘ ⇑h) s x ↔ ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h x)
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : N → M'<VAR>s : Set M<VAR>hm : m ≤ n<GOAL>ContMDiffOn I I' m (f ∘ ⇑h) s ↔ ContMDiffOn J I' m f (⇑h.symm ⁻¹' s)
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : N → M'<VAR>x : M<VAR>hm : m ≤ n<GOAL>ContMDiffAt I I' m (f ∘ ⇑h) x ↔ ContMDiffAt J I' m f (h x)
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : N → M'<VAR>hm : m ≤ n<GOAL>ContMDiff I I' m (f ∘ ⇑h) ↔ ContMDiff J I' m 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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : M' → M<VAR>hm : m ≤ n<VAR>s : Set M'<VAR>x : M'<GOAL>ContMDiffWithinAt I' J m (⇑h ∘ f) s x ↔ ContMDiffWithinAt I' I m f s x
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : M' → M<VAR>hm : m ≤ n<VAR>x : M'<GOAL>ContMDiffAt I' J m (⇑h ∘ f) x ↔ ContMDiffAt I' I m f x
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : M' → M<VAR>hm : m ≤ n<VAR>s : Set M'<GOAL>ContMDiffOn I' J m (⇑h ∘ f) s ↔ ContMDiffOn I' I m f s
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : M' → M<VAR>hm : m ≤ n<GOAL>ContMDiff I' J m (⇑h ∘ f) ↔ ContMDiff I' I m f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>hn : 1 ≤ n<GOAL>PartialHomeomorph.MDifferentiable I J h.toHomeomorph.toPartialHomeomorph
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>G' : Type u_8<VAR>TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>N' : Type u_12<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>n : ℕ∞<VAR>h₁ : M ≃ₘ^n⟮I, I'⟯ M'<VAR>h₂ : N ≃ₘ^n⟮J, J'⟯ N'<GOAL>(h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>G' : Type u_8<VAR>TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>N' : Type u_12<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>n : ℕ∞<VAR>h₁ : M ≃ₘ^n⟮I, I'⟯ M'<VAR>h₂ : N ≃ₘ^n⟮J, J'⟯ N'<GOAL>⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<GOAL>(Diffeomorph.prodComm I J M N n).symm = Diffeomorph.prodComm J I N M n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<GOAL>⇑(Diffeomorph.prodComm I J M N n) = Prod.swap
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners J N<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>hn : 1 ≤ n<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<GOAL>UniqueMDiffOn J (⇑h '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners J N<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>hn : 1 ≤ n<VAR>s : Set M<GOAL>UniqueMDiffOn J (⇑h '' s) ↔ UniqueMDiffOn I s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>SmoothManifoldWithCorners I M<VAR>SmoothManifoldWithCorners J N<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>hn : 1 ≤ n<VAR>s : Set N<GOAL>UniqueMDiffOn I (⇑h ⁻¹' s) ↔ UniqueMDiffOn J s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>hn : 1 ≤ n<VAR>s : Set E<GOAL>UniqueDiffOn 𝕜 (⇑h '' s) ↔ UniqueDiffOn 𝕜 s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>hn : 1 ≤ n<VAR>s : Set F<GOAL>UniqueDiffOn 𝕜 (⇑h ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
<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>e : E ≃L[𝕜] E'<GOAL>⇑e.toDiffeomorph = ⇑e
<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>e : E ≃L[𝕜] E'<GOAL>e.symm.toDiffeomorph = e.toDiffeomorph.symm
<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>e : E ≃L[𝕜] E'<GOAL>⇑e.toDiffeomorph.symm = ⇑e.symm
<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_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<GOAL>↑(I.transDiffeomorph e) = ⇑e ∘ ↑I
<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_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<GOAL>↑(I.transDiffeomorph e).symm = ↑I.symm ∘ ⇑e.symm
<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_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<GOAL>Set.range ↑(I.transDiffeomorph e) = ⇑e '' Set.range ↑I
<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_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<VAR>x : M<GOAL>↑(extChartAt (I.transDiffeomorph e) x) = ⇑e ∘ ↑(extChartAt I x)
<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_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<VAR>x : M<GOAL>↑(extChartAt (I.transDiffeomorph e) x).symm = ↑(extChartAt I x).symm ∘ ⇑e.symm
<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_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<VAR>x : M<GOAL>(extChartAt (I.transDiffeomorph e) x).target = ⇑e.symm ⁻¹' (extChartAt I x).target
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M' → M<VAR>x : M'<VAR>s : Set M'<GOAL>ContMDiffWithinAt I' (I.transDiffeomorph e) n f s x ↔ ContMDiffWithinAt I' I n f s x
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M' → M<VAR>x : M'<GOAL>ContMDiffAt I' (I.transDiffeomorph e) n f x ↔ ContMDiffAt I' I n f x
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M' → M<VAR>s : Set M'<GOAL>ContMDiffOn I' (I.transDiffeomorph e) n f s ↔ ContMDiffOn I' I n f s
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M' → M<GOAL>ContMDiff I' (I.transDiffeomorph e) n f ↔ ContMDiff I' I 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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M' → M<GOAL>Smooth I' (I.transDiffeomorph e) f ↔ Smooth I' I 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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<GOAL>ContMDiffWithinAt (I.transDiffeomorph e) I' n f s x ↔ ContMDiffWithinAt I I' n f s x
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M → M'<VAR>x : M<GOAL>ContMDiffAt (I.transDiffeomorph e) I' n f x ↔ ContMDiffAt I I' n f x
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M → M'<VAR>s : Set M<GOAL>ContMDiffOn (I.transDiffeomorph e) I' n f s ↔ ContMDiffOn I I' n f s
<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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M → M'<GOAL>ContMDiff (I.transDiffeomorph e) I' n f ↔ ContMDiff I I' 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>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>f : M → M'<GOAL>Smooth (I.transDiffeomorph e) I' f ↔ Smooth I I' f
<VAR>H : Type u_1<VAR>TopologicalSpace H<VAR>H' : Type u_2<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>hG : G.LocalInvariantProp G' P<VAR>U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ<VAR>f : (StructureGroupoid.LocalInvariantProp.sheaf M M' hG).val.obj U<GOAL>ChartedSpace.LiftProp P ↑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>x : H<GOAL>HasMFDerivAt I 𝓘(𝕜, E) (↑I) 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>s : Set H<VAR>x : H<GOAL>HasMFDerivWithinAt I 𝓘(𝕜, E) (↑I) 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>s : Set H<VAR>x : H<GOAL>MDifferentiableWithinAt I 𝓘(𝕜, E) (↑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<VAR>x : H<GOAL>MDifferentiableAt I 𝓘(𝕜, E) (↑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<GOAL>MDifferentiableOn I 𝓘(𝕜, E) (↑I) 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>MDifferentiable I 𝓘(𝕜, E) ↑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 : E<VAR>hx : x ∈ Set.range ↑I<GOAL>HasMFDerivWithinAt 𝓘(𝕜, E) I (↑I.symm) (Set.range ↑I) x (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, 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<GOAL>MDifferentiableOn 𝓘(𝕜, E) I (↑I.symm) (Set.range ↑I)