ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L M : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>h' : M ⊆ K<GOAL>SimpleGraph.ComponentCompl.hom ⋯ C = SimpleGraph.ComponentCompl.hom h' (SimpleGraph.ComponentCompl.hom h C)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L : Set V<VAR>v : V<VAR>vnL : v ∉ L<VAR>h : K ⊆ L<GOAL>SimpleGraph.ComponentCompl.hom h (G.componentComplMk vnL) = G.componentComplMk ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>Cinf : (↑C).Infinite<GOAL>(↑(SimpleGraph.ComponentCompl.hom h C)).Infinite
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Finset V<VAR>C : G.ComponentCompl ↑K<GOAL>C.supp.Infinite ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, SimpleGraph.ComponentCompl.hom h D = C
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>∀ {X Y : (Finset V)ᵒᵖ} (f : X ⟶ Y) (C : G.ComponentCompl ↑(Opposite.unop X)), G.componentComplFunctor.map f C = SimpleGraph.ComponentCompl.hom ⋯ C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : (Finset V)ᵒᵖ<GOAL>G.componentComplFunctor.obj K = G.ComponentCompl ↑(Opposite.unop K)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j<VAR>sec : s ∈ G.end<VAR>K L : (Finset V)ᵒᵖ<VAR>h : L ⟶ K<VAR>v : V<VAR>vnL : v ∉ Opposite.unop L<VAR>hs : s L = G.componentComplMk vnL<GOAL>s K = G.componentComplMk ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : (Finset V)ᵒᵖ<VAR>C : G.componentComplFunctor.obj K<GOAL>(SimpleGraph.ComponentCompl.supp C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>W : Type u_2<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>Fintype ↑G.edgeSet<VAR>Fintype ↑G'.edgeSet<GOAL>G.edgeFinset.card = G'.edgeFinset.card
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<GOAL>¬(G.replaceVertex s t).Adj s t
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s : V<GOAL>G.replaceVertex s s = G
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s : V<VAR>t w : V<VAR>hw : w ≠ t<GOAL>(G.replaceVertex s t).Adj s w ↔ G.Adj s w
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s : V<VAR>t w : V<VAR>hw : w ≠ t<GOAL>(G.replaceVertex s t).Adj t w ↔ G.Adj s w
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s : V<VAR>t v w : V<VAR>hv : v ≠ t<VAR>hw : w ≠ t<GOAL>(G.replaceVertex s t).Adj v w ↔ G.Adj v w
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<GOAL>(G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<GOAL>(G.replaceVertex s t).edgeSet = (G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s) \ {s(t, t)}
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset = G.edgeFinset \ G.incidenceFinset t ∪ Finset.image (fun x => s(x, t)) (G.neighborFinset s)
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>ha : G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset = (G.edgeFinset \ G.incidenceFinset t ∪ Finset.image (fun x => s(x, t)) (G.neighborFinset s)) \ {s(t, t)}
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>Fintype V<VAR>DecidableRel G.Adj<GOAL>Disjoint (G.edgeFinset \ G.incidenceFinset t) (Finset.image (fun x => s(x, t)) (G.neighborFinset s))
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t
<VAR>V : Type u_1<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>ha : G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t - 1
<VAR>V : Type u_1<VAR>s t v w : V<GOAL>(SimpleGraph.edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
<VAR>V : Type u_1<VAR>s : V<GOAL>SimpleGraph.edge s s = ⊥
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s : V<GOAL>G ⊔ SimpleGraph.edge s s = G
<VAR>V : Type u_1<VAR>s t : V<VAR>h : s ≠ t<GOAL>(SimpleGraph.edge s t).edgeSet = {s(s, t)}
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s t : V<VAR>h : G.Adj s t<GOAL>G ⊔ SimpleGraph.edge s t = G
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s t : V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Fintype ↑(G ⊔ SimpleGraph.edge s t).edgeSet<VAR>hn : ¬G.Adj s t<VAR>h : s ≠ t<GOAL>(G ⊔ SimpleGraph.edge s t).edgeFinset = Finset.cons s(s, t) G.edgeFinset ⋯
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s t : V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Fintype ↑(G ⊔ SimpleGraph.edge s t).edgeSet<VAR>hn : ¬G.Adj s t<VAR>h : s ≠ t<GOAL>(G ⊔ SimpleGraph.edge s t).edgeFinset.card = G.edgeFinset.card + 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<GOAL>iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<GOAL>(iteratedFDeriv 𝕜 n fun x => 0) = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n fun x => 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>c : F<GOAL>ContDiff 𝕜 n fun x => c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>c : F<VAR>s : Set E<GOAL>ContDiffOn 𝕜 n (fun x => c) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>c : F<GOAL>ContDiffAt 𝕜 n (fun x => c) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>c : F<GOAL>ContDiffWithinAt 𝕜 n (fun x => c) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>Subsingleton F<GOAL>ContDiff 𝕜 n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>Subsingleton F<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>Subsingleton F<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>Subsingleton F<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>n : ℕ<VAR>c : F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>c : F<GOAL>(iteratedFDeriv 𝕜 (n + 1) fun x => c) = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 n (fun x => c) s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : F<GOAL>(iteratedFDeriv 𝕜 n fun x => c) = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>ContDiff 𝕜 n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E →L[𝕜] F<GOAL>ContDiff 𝕜 n ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E ≃L[𝕜] F<GOAL>ContDiff 𝕜 n ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E →ₗᵢ[𝕜] F<GOAL>ContDiff 𝕜 n ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E ≃ₗᵢ[𝕜] F<GOAL>ContDiff 𝕜 n ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n id
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>s : Set E<VAR>x : E<GOAL>ContDiffWithinAt 𝕜 n id s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>x : E<GOAL>ContDiffAt 𝕜 n id x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>s : Set E<GOAL>ContDiffOn 𝕜 n id s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>n : ℕ∞<VAR>hb : IsBoundedBilinearMap 𝕜 b<GOAL>ContDiff 𝕜 n b
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : F →L[𝕜] G<VAR>hf : HasFTaylorSeriesUpToOn n f p s<GOAL>HasFTaylorSeriesUpToOn n (⇑g ∘ f) (fun x k => g.compContinuousMultilinearMap (p x k)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>g : F →L[𝕜] G<VAR>hf : ContDiffWithinAt 𝕜 n f s x<GOAL>ContDiffWithinAt 𝕜 n (⇑g ∘ f) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>g : F →L[𝕜] G<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (⇑g ∘ f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>g : F →L[𝕜] G<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (⇑g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : F →L[𝕜] G<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => g (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : F →L[𝕜] G<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : F →L[𝕜] G<VAR>hf : ContDiff 𝕜 n f<VAR>x : E<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDeriv 𝕜 i (⇑g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x : E<VAR>g : F ≃L[𝕜] G<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<GOAL>iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : F →ₗᵢ[𝕜] G<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : F →ₗᵢ[𝕜] G<VAR>hf : ContDiff 𝕜 n f<VAR>x : E<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x : E<VAR>g : F ≃ₗᵢ[𝕜] G<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F ≃ₗᵢ[𝕜] G<VAR>f : E → F<VAR>x : E<VAR>i : ℕ<GOAL>‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>e : F ≃L[𝕜] G<GOAL>ContDiffWithinAt 𝕜 n (⇑e ∘ f) s x ↔ ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>e : F ≃L[𝕜] G<GOAL>ContDiffAt 𝕜 n (⇑e ∘ f) x ↔ ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>e : F ≃L[𝕜] G<GOAL>ContDiffOn 𝕜 n (⇑e ∘ f) s ↔ ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>n : ℕ∞<VAR>e : F ≃L[𝕜] G<GOAL>ContDiff 𝕜 n (⇑e ∘ f) ↔ ContDiff 𝕜 n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFTaylorSeriesUpToOn n f p s<VAR>g : G →L[𝕜] E<GOAL>HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>x : G<VAR>g : G →L[𝕜] E<VAR>hf : ContDiffWithinAt 𝕜 n f s (g x)<GOAL>ContDiffWithinAt 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>hf : ContDiffOn 𝕜 n f s<VAR>g : G →L[𝕜] E<GOAL>ContDiffOn 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : G →L[𝕜] E<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n (f ∘ ⇑g)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : G →L[𝕜] E<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>h's : UniqueDiffOn 𝕜 (⇑g ⁻¹' s)<VAR>x : G<VAR>hx : g x ∈ s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x = (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>g : G ≃L[𝕜] E<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : G<VAR>hx : g x ∈ s<VAR>i : ℕ<GOAL>iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x = (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>g : G →L[𝕜] E<VAR>f : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>x : G<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDeriv 𝕜 i (f ∘ ⇑g) x = (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun x => g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>g : G ≃ₗᵢ[𝕜] E<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : G<VAR>hx : g x ∈ s<VAR>i : ℕ<GOAL>‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : G ≃ₗᵢ[𝕜] E<VAR>f : E → F<VAR>x : G<VAR>i : ℕ<GOAL>‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>e : G ≃L[𝕜] E<GOAL>ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (⇑e ⁻¹' s) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>e : G ≃L[𝕜] E<GOAL>ContDiffAt 𝕜 n (f ∘ ⇑e) (e.symm x) ↔ ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>e : G ≃L[𝕜] E<GOAL>ContDiffOn 𝕜 n (f ∘ ⇑e) (⇑e ⁻¹' s) ↔ ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>n : ℕ∞<VAR>e : G ≃L[𝕜] E<GOAL>ContDiff 𝕜 n (f ∘ ⇑e) ↔ ContDiff 𝕜 n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFTaylorSeriesUpToOn n f p s<VAR>g : E → G<VAR>q : E → FormalMultilinearSeries 𝕜 E G<VAR>hg : HasFTaylorSeriesUpToOn n g q s<GOAL>HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : E → F<VAR>g : E → G<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => (f x, g x)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : E → F<VAR>g : E → G<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g s<GOAL>ContDiffOn 𝕜 n (fun x => (f x, g x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : E → G<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => (f x, g x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F<VAR>g : E → G<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n fun x => (f x, g x)